src/HOL/NumberTheory/Fib.thy
changeset 11868 56db9f3a6b3e
parent 11786 51ce34ef5113
child 15003 6145dd7538d7
     1.1 --- a/src/HOL/NumberTheory/Fib.thy	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/Fib.thy	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -67,8 +67,8 @@
     1.4  *}
     1.5  
     1.6  lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
     1.7 -  (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
     1.8 -   else int (fib (Suc n) * fib (Suc n)) + Numeral1)"
     1.9 +  (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1
    1.10 +   else int (fib (Suc n) * fib (Suc n)) + 1)"
    1.11    apply (induct n rule: fib.induct)
    1.12      apply (simp add: fib.Suc_Suc)
    1.13     apply (simp add: fib.Suc_Suc mod_Suc)