proposition: Theorem fib_2n_plus_2 : forall n, fib (S (2*n+1)) = fib (n+1) * (fib (n+1)) + fib n * fib n.
proof: Proof. intros n; replace (S (2*n+1)) with ((n+1)+(n+1)) by ring. rewrite fib_n_p'. replace (n + 1 + 1) with (S (S n)) by ring. rewrite fib_SSn. replace (S n) with (n + 1) by ring. rewrite (Nat.add_comm (fib n) (fib (n + 1))). now rewrite sub_add. Qed.
imports: Arith ArithRing ZArith fib_ind OldArith