proposition: Lemma general_fib_2 : forall a b n:nat, general_fib a b (S (S n)) = general_fib a b n + general_fib a b (S n).
proof: Proof. intros a b n; generalize a b; induction n as [ | n IHn]. - reflexivity. - clear a b; intros a b. rewrite (general_fib_S _ _ (S (S n))), IHn. now rewrite (general_fib_S _ _ (S n)). Qed.
imports: Arith fib_ind