(n m k : nat) : (n + k) - m <= (n - m) + k. Proof. simple_induction k k IHk. - destruct (nat_add_zero_r n)^, (nat_add_zero_r (n - m))^; constructor. - destruct (nat_add_succ_r n k)^. refine (leq_trans (nataddsub_comm_ineq_lemma (n+k) m) _). destruct (nat_add_succ_r (n - m) k)^. by apply leq_succ. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.