proposition: Theorem comp_ind: forall P: nat -> Prop, (forall n: nat, (forall m: nat, m < n -> P m) -> P n) -> forall n:nat, P n.
proof: Proof. intros P H n. assert (forall n:nat , forall m:nat, m < n -> P m). intro n0. induction n0 as [| n']; intros. inversion H0. apply le_S_n in H0. apply le_lt_or_eq in H0. sp; subst; sp. apply H0 with (n := S n). auto. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega