proposition: Lemma fib_SSn_p : forall n p:nat, fib (S (S p) + n) = fib (S n) * fib (S p) + fib n * fib p.
proof: Proof. intro n; induction n as [ | | n Hn HSn] using fib_ind. - cbn;intros; repeat rewrite Nat.add_0_r; rewrite Nat.add_comm; auto. - intro p; replace (S (S p) + 1) with (S (S (S p))) by ring. rewrite (fib_SSn (S p)); simpl (fib 2); simpl (fib 1); rewrite (fib_SSn p); ring. - intros p. replace (S (S p) + S (S n)) with (S (S (S (S p) + n))) by ring. rewrite (fib_SSn (S (S p) + n)), Hn. replace (S (S (S p) + n)) with (S (S p) + S n) by ring. rewrite HSn; rewrite (fib_SSn (S n)); rewrite (fib_SSn n). ring. Qed.
imports: Arith