src/HOL/Number_Theory/Fib.thy
 changeset 60688 01488b559910 parent 60527 eb431a5651fe child 61649 268d88ec9087
equal inserted replaced
60687:33dbbcb6a8a3 60688:01488b559910
`    65 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"`
`    65 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"`
`    66   apply (simp add: gcd_commute_nat [of "fib m"])`
`    66   apply (simp add: gcd_commute_nat [of "fib m"])`
`    67   apply (cases m)`
`    67   apply (cases m)`
`    68   apply (auto simp add: fib_add)`
`    68   apply (auto simp add: fib_add)`
`    69   apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat`
`    69   apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat`
`    70     gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)`
`    70     gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute)`
`    71   done`
`    71   done`
`    72 `
`    72 `
`    73 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"`
`    73 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"`
`    74   by (simp add: gcd_fib_add [symmetric, of _ "n-m"])`
`    74   by (simp add: gcd_fib_add [symmetric, of _ "n-m"])`
`    75 `
`    75 `