proposition: Theorem fib_2n_plus_1 : forall n, fib (2*n+1) = 2 * fib n * fib (n+1) - fib n * fib n.
proof: Proof. intros n; replace (2*n+1) with (n + (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))). rewrite sub_add. apply Nat.add_cancel_l with (fib n * fib n). rewrite le_add_sub_r. rewrite Nat.add_shuffle3. rewrite Nat.mul_sub_distr_r. rewrite le_add_sub_r. ring. apply Nat.mul_le_mono_r. apply fib_monotonic. replace (fib n * fib n) with (1 * (fib n * fib n)). rewrite <- Nat.mul_assoc. apply Nat.mul_le_mono; auto with arith. apply Nat.mul_le_mono_l. apply fib_monotonic. ring. Qed.
imports: Arith ArithRing ZArith fib_ind OldArith