Let $\mathbb{N}$ be the set of \reftext{def:natural-numbers-2026a}{natural numbers}, with addition $+$ and successor map $S$ as in that definition, and let $<$ and $\le$ be the \reftext{def:order-natural-numbers-2026a}{order relations} of that definition. Then the following hold for all $j,k,m,n,p,t,y\in\mathbb{N}$.

1. $m\le m$; if $m<n$ then $m\le n$; if $m<n$ and $n<p$ then $m<p$; and if $m\le n$ and $n\le p$ then $m\le p$.
2. $m<m$ is false; $m<n$ and $n<m$ do not both hold; and if $m\le n$ and $n\le m$ then $m=n$.
3. (\textit{Trichotomy}) Exactly one of $m<n$, $m=n$, $n<m$ holds.
4. $1\le m$.
5. $m<S(m)$; and if $k\le S(m)$ and $k\ne S(m)$, then $k\le m$.
6. $m<m+j$; if $j\le t$ then $m+j\le m+t$; and if $m\le n$ then $S(m)\le S(n)$.
7. If $m<y$, then there is exactly one $k\in\mathbb{N}$ with $y=m+k$.