Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).

--- a/src/HOL/ex/Fib.ML	Sat Dec 06 17:05:41 1997 +0100
+++ b/src/HOL/ex/Fib.ML	Sat Dec 06 17:06:21 1997 +0100
@@ -39,6 +39,12 @@
 qed "fib_Suc_neq_0";
 Addsimps [fib_Suc_neq_0];
 
+goal thy "0 < fib (Suc n)";
+by (res_inst_tac [("u","n")] fib.induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules)));
+qed "fib_Suc_gr_0";
+Addsimps [fib_Suc_gr_0];
+
 
 
 (*Concrete Mathematics, page 278: Cassini's identity*)