proposition: Lemma lt_equiv : forall n m, lt_alt n m <-> n < m.
proof: Proof. intros n m; split. - intros (p,H). rewrite <- H, add_succ_l, lt_succ_r, add_comm. apply le_add_r. - intro H. exists (m-S n). rewrite add_succ_l, <- add_succ_r. apply sub_add. now rewrite le_succ_l. Qed.
imports: NMulOrder