proposition: Lemma forall_num_lt_d : forall m P, (forall n, n < S m -> P n) -> P 0 # (forall n, n < m -> P (S n) ).
proof: Proof. introv Hlt. dimp (Hlt 0); auto; [omega|]. dands; auto. introv Hgt. apply lt_n_S in Hgt. eauto. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega