proposition: Lemma lt_S_case : forall (m n:nat), (lt m (S n)) -> (lt m n) \/ (m=n).
proof: Proof. intros m n. generalize m. induction n. intros. rewrite (lt_1_0 m0 H). tauto. destruct m0. intro. auto with arith. intro. elim IHn with (m:=m0); auto with arith. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef