proposition: Theorem fib_2n : forall n, fib (2*n) = fib (n) * fib (n) + (fib (n+1) - fib n)*(fib (n+1) - fib n).
proof: Proof. intros n; replace (2*n) with (n+n) by ring. apply fib_n_p'. Qed.
imports: Arith ArithRing ZArith fib_ind OldArith