# Proof of basic subtraction rules for natural numbers

For $$m, n ∈ \mathbb{N}_0$$ we define a relation $$≥$$ by $$m ≥ n ⇔ ∃r ∈ \mathbb{N}_0, m = r + n$$. We denote $$r$$ by the difference $$m - n$$ which is thus defined only when m ≥ n.

How can we verify the basic subtraction rules involving natural number, specifically:

1. $$m – (n – r) = (m – n) + r$$ for $$m ≥ n ≥ r$$,
2. $$m + (n – r) = (m + n) – r$$ for $$n ≥ r$$,
3. $$m(n – r) = mn – mr$$ for $$n ≥ r$$.

E.g. for 3 we can set $$n = s + r$$ and thus $$mn = m(s + r) = ms + mr$$, which by definition $$mn – mr = ms = m(n – r)$$ since $$s = n – r$$.

Any hint in the right direction would be welcome. Thanks in advance.

Since (3.) is shown already in the question itself, I detailed below only the presumed proofs for (1.) and (2.).

For (1.) setting $$n=s+r$$ since $$n ≥ r$$ and $$m=w+n$$ since $$m ≥ n$$ thus

• $$m - n = w$$ since $$m ≥ n$$
• $$m = w + n = w + (s + r)$$ since $$m ≥ n$$ and $$n ≥ r$$
• $$m = w + (s + r) = w + (r + s) = (w + r) + s$$ by associativity and commutativity of addition
• $$m = ((m - n) + r) + (n - r)$$ by definition
• $$m - (n - r) = ((m - n) + r) = (m - n) + r$$ by definition since $$m ≥ n$$ and by extension $$m ≥ s$$

For (2.) setting $$n=s + r$$ since $$n ≥ r$$ thus

• $$m + n = m + (s + r)$$
• $$m + n = (m + s) + r$$ by associativity of addition
• $$m + s = (m + n) - r$$ by definition, since $$n ≥ r$$
• $$m + (n-r) = (m + n) - r$$ since $$s = n - r$$

I would still appreciate a double check.