| changeset 15003 | 6145dd7538d7 |
| parent 11868 | 56db9f3a6b3e |
| child 15439 | 71c0f98e31f1 |
--- a/src/HOL/NumberTheory/Fib.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/NumberTheory/Fib.thy Thu Jun 24 17:52:02 2004 +0200 @@ -66,7 +66,8 @@ much easier to prove using integers! *} -lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) = +lemma fib_Cassini: + "int (fib (Suc (Suc n)) * fib n) = (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1 else int (fib (Suc n) * fib (Suc n)) + 1)" apply (induct n rule: fib.induct)