proposition: Lemma lt_S_r : forall (n1 n2:nat), (lt n1 n2) -> exists (n:nat), n2 = (S n).
proof: Proof. destruct n2. intro. exfalso. apply (Nat.nlt_0_r n1). assumption. intro. exists n2. trivial. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef