Order and Arithmetic of ℕ₀ in Flat Form

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathbb{N}_{0}$, $\mathbb{N}$, $0$ and $1$ be as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), $+$ and $\cdot$ the addition and multiplication, $\le$ and $<$ the order and strict order of $\mathbb{N}_{0}$, and $[n]$ the segment. Let $m,n,p\in\mathbb{N}_{0}$ and $q\in\mathbb{N}$.

(i) Order. $n\le n$; if $m\le n$ and $n\le p$ then $m\le p$; if $m\le n$ and $n\le m$ then $m=n$; $m\le n$ or $n\le m$; $0\le n$; $n\le n+m$; $n<n+1$; and

$$m<n\iff\bigl(m\le n\text{ and }m\neq n\bigr),\qquad m<n+1\iff m\le n.$$

(ii) Successor. The successor of $n$ is $n+1$; $n+1\neq0$; $1\in\mathbb{N}_{0}$; and $n+1\in\mathbb{N}_{0}$.

(iii) Addition. $m+n\in\mathbb{N}_{0}$, and

$$m+0=m,\qquad 0+m=m,\qquad m+n=n+m,\qquad (m+n)+p=m+(n+p).$$

(iv) Cancellation. If $m+p=n+p$, then $m=n$; if $p+m=p+n$, then $m=n$.

(v) Multiplication. $m\cdot n\in\mathbb{N}_{0}$, and

$$m\cdot1=m,\qquad m\cdot n=n\cdot m,\qquad m\cdot0=0,\qquad (m\cdot n)\cdot p=m\cdot(n\cdot p),\qquad m\cdot(n+p)=m\cdot n+m\cdot p.$$

(vi) Natural numbers. For every class $x$: $x\in\mathbb{N}$ if and only if $x=j+1$ for some $j\in\mathbb{N}_{0}$. Every element of $\mathbb{N}$ lies in $\mathbb{N}_{0}$, and $q+m\in\mathbb{N}$.

(vii) Segments. $q\in[q]$; every element of $[n]$ lies in $[n+1]$ and in $\mathbb{N}$; and $[n]$ is finite.