proposition: Lemma recur2 : forall P : nat -> Prop, (forall n : nat, (forall p : nat, p < n -> P p) -> P n) -> forall m : nat, P m.
proof: Proof. intros; apply H; elim m. intros; absurd (p < 0); auto with arith. intros; case (le_lt_eq_dec p n). auto with arith. auto with arith. intro; rewrite e; apply H; auto. Qed.
imports: ZArith Omega