Division with remainder in $\mathbb{Z}$: for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < b$

Sums and products of nonnegative integers are nonnegative: if $0 \le u$ and $0 \le v$ then $u \le u + v$ by compatibility with addition, so $0 \le u + v$ by transitivity; and if either factor is $0$ then $uv = 0$, while if both are positive then $0 < uv$.

Discreteness: if $0 < x$ in $\mathbb{Z}$ then $1 \le x$. Indeed $x$ is nonnegative, so $x = \iota(k)$ for some $k \in \mathbb{N}$, and $k \ne 0$ because $\iota(0) = 0 \ne x$; hence $k = \sigma(j) = 1 + j$ for some $j$, so $1 \le k$ in $\mathbb{N}$, and applying $\iota$, which preserves the order, gives $1 = \iota(1) \le \iota(k) = x$.

$\iota$ reflects the order: if $\iota(m) < \iota(n)$ then $m < n$. For otherwise trichotomy on $\mathbb{N}$ gives $n \le m$, whence $\iota(n) \le \iota(m)$ because $\iota$ preserves the order, and this together with $\iota(m) < \iota(n)$ contradicts antisymmetry.

Write $a = \iota(a_1) - \iota(a_2)$ with $a_1, a_2 \in \mathbb{N}$, which is possible because $a = [(a_1,a_2)]$ for some naturals and $[(a_1,a_2)] = [(a_1,0)] + [(0,a_2)] = \iota(a_1) - \iota(a_2)$.

Uniqueness. Suppose $a = q_1 b + r_1 = q_2 b + r_2$ with $0 \le r_i < b$ for $i = 1, 2$, and set $d := q_1 - q_2$. Ring arithmetic gives $d b = r_2 - r_1$.

From $0 < b$ and step 1.2, $1 \le b$, so $0 \le b - 1$ by compatibility with addition.

Put $q_0 := -\iota(a_2)$. Then $a - q_0 b = a + \iota(a_2) b = \bigl(\iota(a_1) - \iota(a_2)\bigr) + \iota(a_2) b = \iota(a_1) + \iota(a_2)(b - 1)$, by ring arithmetic.

If $0 < d$ then $1 \le d$ by step 1.2, so $0 \le d - 1$ and hence $0 \le (d-1)b$ by step 1.1, that is $b \le db$; but $r_1 \ge 0$ gives $r_2 - r_1 \le r_2 < b$, so $b \le db = r_2 - r_1 < b$, contradicting antisymmetry.

If $d < 0$ then $0 < -d$, and the same computation with the roles of the two pairs interchanged, using $(-d)b = r_1 - r_2$, gives $b \le r_1 - r_2 < b$, again a contradiction.

The integer $a - q_0 b$ is nonnegative: $\iota(a_1) \ge 0$ and $\iota(a_2) \ge 0$ because both lie in the image of $\iota$, $b - 1 \ge 0$ by step 2.1, and sums and products of nonnegative integers are nonnegative.

Hence $d = 0$ by totality, so $q_1 = q_2$, and then $r_1 = a - q_1 b = a - q_2 b = r_2$.

Hence the set $T := \{\, k \in \mathbb{N} : \iota(k) = a - qb \text{ for some } q \in \mathbb{Z} \,\}$ is nonempty, since $a - q_0 b$ is a nonnegative integer and therefore equals $\iota(k)$ for some $k \in \mathbb{N}$.

By well-ordering let $r_0$ be the least element of $T$, choose $q \in \mathbb{Z}$ with $\iota(r_0) = a - qb$, and set $r := \iota(r_0)$. Then $a = qb + r$ and $0 \le r$.

Suppose $b \le r$. Then $0 \le r - b$ by compatibility with addition, and $r - b = (a - qb) - b = a - (q+1)b$ by ring arithmetic, so $r - b = \iota(k')$ for some $k' \in \mathbb{N}$ with $k' \in T$. Also $-b < 0$, since $0 < b$, so $r - b < r$, that is $\iota(k') < \iota(r_0)$, whence $k' < r_0$ by step 1.3. This contradicts the minimality of $r_0$.

Therefore $b \le r$ fails, and by totality of the order $r < b$; with step 5.1 this establishes existence of a pair $(q,r)$ with $a = qb + r$ and $0 \le r < b$.

Existence is step 7.1 and uniqueness is step 3.2, so for every $a \in \mathbb{Z}$ and every $b > 0$ there is exactly one pair $(q,r)$ of integers with $a = qb + r$ and $0 \le r < b$.