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