equal
deleted
inserted
replaced
83 theorem fib_Cassini: |
83 theorem fib_Cassini: |
84 "fib (Suc (Suc n)) * fib n = |
84 "fib (Suc (Suc n)) * fib n = |
85 (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1 |
85 (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1 |
86 else fib (Suc n) * fib (Suc n) + 1)" |
86 else fib (Suc n) * fib (Suc n) + 1)" |
87 apply (rule int_int_eq [THEN iffD1]) |
87 apply (rule int_int_eq [THEN iffD1]) |
88 apply (simp add: fib_Cassini_int del: of_nat_mult) |
88 apply (simp add: fib_Cassini_int) |
89 apply (subst zdiff_int [symmetric]) |
89 apply (subst zdiff_int [symmetric]) |
90 apply (insert fib_Suc_gr_0 [of n], simp_all) |
90 apply (insert fib_Suc_gr_0 [of n], simp_all) |
91 done |
91 done |
92 |
92 |
93 |
93 |