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 Hstep n. assert (H : P n /\ P (S n)) by (elim n; intuition). now destruct H. Qed.
imports: Arith ArithRing Lia Wf_nat