proposition: Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.
proof: Proof. intros n m p. destruct (le_ge_cases p m) as [LE|GE]. - rewrite <- (sub_add p m) at 1 by assumption. now rewrite <- add_lt_mono_r. - assert (GE' := GE). rewrite <- sub_0_le in GE'; rewrite GE'. split; intros LT. + elim (lt_irrefl m). apply le_lt_trans with (n+p); trivial. rewrite <- (add_0_l m). apply add_le_mono. * apply le_0_l. * assumption. + now elim (nlt_0_r n). Qed.
imports: NMulOrder