proposition: Theorem fib_fib2_equiv : forall n, fib n = (fst (fib2 n)).
proof: Proof. intros n; elim n using fib_ind; try(simpl;auto with arith;fail). intros p IHp IHSp. replace (fib (S (S p))) with (fib p + fib (S p)). rewrite IHp; rewrite IHSp. simpl. case (fib2 p); auto. auto. Qed.
imports: Arith ArithRing