proposition: Proposition natpmswap2 (k m n : nat) : n <= k -> k - n <= m -> k <= n + m.
proof: Proof. intros l q. apply (@nataddpreservesleq' (k - n) m n) in q. destruct (symmetric_paths _ _ (nataddsub_assoc n l)) in q. destruct (symmetric_paths _ _ (add_n_sub_n_eq' k n)) in q; assumption. Defined.
imports: Basics Spaces.Nat.Core