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 (P n/\P(S n)). elim n; intuition. intuition. Qed.
imports: Arith ArithRing