equal
deleted
inserted
replaced
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 |