proposition: Theorem le_sub_le_add_r : forall n m p, n - p <= m <-> n <= m + p.
proof: Proof. intros n m p. split; intros LE. - rewrite (add_le_mono_r _ _ p) in LE. apply le_trans with (n-p+p); auto using sub_add_le. - destruct (le_ge_cases n p) as [LE'|GE]. + rewrite <- sub_0_le in LE'. rewrite LE'. apply le_0_l. + rewrite (add_le_mono_r _ _ p). now rewrite sub_add. Qed.
imports: NMulOrder