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