proposition: Theorem th_fib_positive1 : forall p : positive, forall u v : nat, u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p)) -> 2*u*v - u*u = fib(nat_of_P (xI p)) /\ v*v + u*u = fib(S (nat_of_P (xI p))).
proof: Proof. intros p u v [Hu Hv]; rewrite Hu; rewrite Hv. rewrite nat_of_P_xI. replace (S (2* nat_of_P p)) with (2*nat_of_P p + 1) by ring. rewrite fib_2n_plus_1, fib_2n_plus_2. replace (S (nat_of_P p)) with (nat_of_P p + 1) by ring; auto. Qed.
imports: Arith ArithRing ZArith fib_ind OldArith