Proof of basic subtraction rules for natural numbers

Question

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.

Answer 1

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.