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