proposition: Theorem fib_n_p' : forall n p, fib (n + p) = fib n * fib p + (fib (n+1) - fib n) *(fib (p+1) - fib p).
proof: Proof. intros n; induction n as [ | | n IHn IHSn] using fib_ind. - intros p; simpl; ring. - intros p; replace (1 + p) with (p + 1) by ring; simpl. ring_simplify. rewrite le_add_sub_r. + reflexivity. + apply fib_monotonic. - intro p; simpl (S (S n) + p);rewrite fib_SSn. replace (S (n + p)) with (S n + p) by ring. rewrite IHn, IHSn; simpl (S (S n)+1). replace (S n + 1) with (S (S n)) by ring. replace (S (n + 1)) with (S (S n)) by ring. repeat rewrite fib_SSn. rewrite (Nat.add_comm (fib (S n)) (fib n + fib (S n))). rewrite sub_add. rewrite (Nat.add_comm (fib n) (fib (S n))). rewrite sub_add. rewrite Nat.mul_sub_distr_r. replace (fib n * fib p + (fib (n + 1) * (fib (p + 1) - fib p) - fib n * (fib (p + 1) - fib p)) + (fib (S n) * fib p + fib n * (fib (p + 1) - fib p))) with (fib n * fib p + (fib n * (fib (p + 1) - fib p) + (fib (n + 1) * (fib (p + 1) - fib p) - fib n * (fib (p + 1) - fib p))) + fib (S n) * fib p) by ring. rewrite (le_add_sub_r). replace (n + 1) with (S n) by ring. ring. apply Nat.mul_le_mono_r. apply fib_monotonic. Qed.
imports: Arith ArithRing ZArith fib_ind OldArith