proposition: Theorem comp_ind_type : forall P: nat -> Type, (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. omega. destruct (eq_nat_dec m n'); subst; auto. apply IHn'; omega. apply H; apply X. Defined.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega