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