proposition: Lemma fib_ind (P:nat->Prop) : P 0%nat -> P 1%nat -> (forall n, P n -> P (S n) -> P(S (S n))) -> forall n, P n.
proof: Proof. intros H0 H1 HS n; assert (P n /\ P (S n)). { induction n. - split;auto. - destruct IHn; split; auto. } tauto. Qed.
imports: Coq(NArith Ring) additions(Monoid_instances Euclidean_Chains Pow Strategies Dichotomy BinaryStrat)