proposition: Proposition nataddpreservesleq { n m k : nat } : n <= m -> n + k <= m + k.
proof: Proof. intro l. simple_induction k k IHk. - destruct (add_n_O n), (add_n_O m); exact l. - destruct (nat_add_n_Sm n k), (nat_add_n_Sm m k); apply leq_S_n'; exact IHk. Defined.
imports: Basics Spaces.Nat.Core