proposition: Proposition nataddsub_comm (n m k : nat) : m <= n -> (n - m) + k = (n + k) - m.
proof: Proof. intro l. destruct (nat_add_comm k n). destruct (nataddsub_assoc k l). apply nat_add_comm. Defined.
imports: Basics Spaces.Nat.Core