src/HOL/NumberTheory/Fib.thy
changeset 11377 0f16ad464c62
parent 11049 7eef34adb852
child 11468 02cd5d5bc497
     1.1 --- a/src/HOL/NumberTheory/Fib.thy	Sat Jun 16 20:06:42 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/Fib.thy	Mon Jun 25 15:35:59 2001 +0200
     1.3 @@ -74,6 +74,8 @@
     1.4     apply (simp add: fib.Suc_Suc mod_Suc)
     1.5    apply (simp add: fib.Suc_Suc
     1.6      add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
     1.7 +  apply (subgoal_tac "x mod #2 < #2", arith)
     1.8 +  apply simp
     1.9    done
    1.10  
    1.11