equal
deleted
inserted
replaced
104 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" |
104 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" |
105 apply (simp add: gcd_commute [of "fib m"]) |
105 apply (simp add: gcd_commute [of "fib m"]) |
106 apply (case_tac m) |
106 apply (case_tac m) |
107 apply simp |
107 apply simp |
108 apply (simp add: fib_add) |
108 apply (simp add: fib_add) |
109 apply (simp add: add_commute gcd_non_0 [OF fib_Suc_gr_0]) |
109 apply (simp add: add.commute gcd_non_0 [OF fib_Suc_gr_0]) |
110 apply (simp add: gcd_non_0 [OF fib_Suc_gr_0, symmetric]) |
110 apply (simp add: gcd_non_0 [OF fib_Suc_gr_0, symmetric]) |
111 apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel) |
111 apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel) |
112 done |
112 done |
113 |
113 |
114 lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |
114 lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |