proposition: Theorem fib_n_p : forall n p, fib(n + p + 2) = fib (n + 1) * fib (p + 1) + fib n * fib p.
proof: Proof. intros n; elim n using fib_ind. - intros p; replace (0 + p+2) with (S (S p)) by ring. replace (p+1) with (S p) by ring. rewrite fib_SSn; simpl; ring. - intros p; replace (1+p+2) with (S (S (S p))) by ring. simpl (fib (1+1)); simpl (fib 1). replace (p+1) with (S p) by ring. repeat rewrite fib_SSn; ring. - intros n' IHn' IHn'1 p. replace (S (S n') + p + 2) with (S (S (n'+p + 2))) by ring. simpl (S (S n') + 1); repeat rewrite fib_SSn. replace (S (n'+p+2)) with (S n' +p+2) by ring. rewrite IHn'1, IHn'. replace (S n'+1) with (S (S n')) by ring. replace (S (n'+1)) with (S (S n')) by ring. rewrite fib_SSn; ring. Qed.
imports: Arith ArithRing ZArith fib_ind OldArith