proposition: Proposition nataddsub_comm_ineq (n m k : nat) : (n + k) - m <= (n - m) + k.
proof: Proof. simple_induction k k IHk. - destruct (add_n_O n), (add_n_O (n - m)); constructor. - destruct (add_n_Sm n k). refine (leq_trans (nataddsub_comm_ineq_lemma (n+k) m) _). destruct (add_n_Sm (n - m) k). now apply leq_S_n'. Defined.
imports: Basics Spaces.Nat.Core