src/HOL/Number_Theory/Fib.thy
changeset 61649 268d88ec9087
parent 60688 01488b559910
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -51,7 +51,7 @@
     1.4  lemma fib_Cassini_nat:
     1.5    "fib (Suc (Suc n)) * fib n =
     1.6       (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
     1.7 -  using fib_Cassini_int [of n] by auto
     1.8 +  using fib_Cassini_int [of n]  by (auto simp del: of_nat_mult of_nat_power)
     1.9  
    1.10  
    1.11  subsection \<open>Law 6.111 of Concrete Mathematics\<close>