proposition: Lemma lt_1_0 : forall (n:nat), (lt n 1) -> (n=0).
proof: Proof. destruct n. auto. intro. inversion H. exfalso. apply (Nat.nle_succ_0 (S n)). assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef