proposition: Proposition natpmswap1 (k m n : nat) : n <= k -> k < n + m -> k - n < m.
proof: Proof. intros l q. assert (q' : k - n + n < m + n) by (destruct (symmetric_paths _ _ (natminuspluseq n k l)); destruct (nat_add_comm n m); assumption). exact (nataddreflectslt q'). Defined.
imports: Basics Spaces.Nat.Core