proposition: Lemma fib_ind : forall P:nat -> Prop, P 0 -> P 1 -> (forall n:nat, P n -> P (S n) -> P (S (S n))) -> forall n:nat, P n.
proof: Proof. intros P H0 H1 HSSn n. assert (H2 : P n /\ P (S n)). - induction n ;[tauto | ]. destruct IHn;split;auto. - destruct H2; auto. Qed.
imports: List Arith Lia