proposition: Proposition nataddpreserveslt { n m k : nat } : n < m -> n + k < m + k.
proof: Proof. unfold "<". change (n + k).+1 with (n.+1 + k). generalize (n.+1). intros n' 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