proposition: Proposition nataddpreserveslt' { n m k : nat } : n < m -> k + n < k + m.
proof: Proof. destruct (symmetric_paths _ _ (nat_add_comm k n)), (symmetric_paths _ _ (nat_add_comm k m)); exact nataddpreserveslt. Defined.
imports: Basics Spaces.Nat.Core