proposition: Lemma minus_lt_S : forall (n1 n2:nat), (lt n1 n2) -> exists (n:nat), (minus n2 n1) = (S n).
proof: Proof. intros. elim (lt_S_r n1 n2 H). intros n H1. rewrite H1. exists (minus n n1). rewrite Nat.sub_succ_l. trivial. apply le_S_n. rewrite H1 in H. auto. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef