proposition: Theorem div2_ind : forall P:nat->Prop, P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
proof: Proof. intros P H0 H1 HS n ; assert (H' : P n /\ P (S n)). - induction n; intuition. - now destruct H'. Qed.
imports: Arith Lia