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