proposition: Proposition natpmswap4 (k m n : nat) : k - n < m -> k < n + m.
proof: Proof. intro l; apply (@nataddpreserveslt (k - n) m n) in l. destruct (nat_add_comm m n). now apply (mixed_trans1 k (k - n + n) (m + n) (nat_sub_add_ineq _ _)). Defined.
imports: Basics Spaces.Nat.Core