Proof of The Sum of $n$ Ones is Strictly Increasing in $n$

Field axioms are numbered as in Field and order axioms as in Ordered Field; the order $\le$ on $\mathbb{R}$ is a total order, hence reflexive, transitive and antisymmetric. Write (O$k$) for claim $k$ of Properties of the Order on the Natural Numbers and (S$k$) for claim $k$ of Properties of Finite Sums.

Step 0.

(a) $0\le 1$. By field axiom 6, $1\ne 0$. Let $t=|1|$ be the absolute value of $1$. By claim 1 of Properties of the Absolute Value in an Ordered Field we have $0\le t$, and $t\ne 0$, since that claim gives $t=0$ only for $1=0$. By claim 4 of the same lemma with $x=y=1$,

Multiplying by the inverse $t^{-1}$ supplied by field axiom 7 and using field axioms 5 and 6,

so $0\le t$ reads $0\le 1$.

(b) For every $x\in\mathbb{R}$ one has $x\le x+1$, and $x+1\le x$ is false. Order axiom 1 with $c=x$ turns $0\le 1$ into $0+x\le 1+x$, that is, $x\le x+1$. If also $x+1\le x$, then order axiom 1 with $c=-x$ gives $(x+1)+(-x)\le x+(-x)=0$, whose left-hand side is $1+(x+(-x))=1$; so $1\le 0$, and antisymmetry with $0\le 1$ gives $1=0$, contradicting field axiom 6.

Step 1: claim 1. By (S1), $\sigma(1)=\mathbf{1}^{(1)}_{1}=1$. Fix $n\in\mathbb{N}$. By (O4), (O5) and (O1) we have $1\le n$ and $n\le S(n)$, so $n\in[S(n)]$ and the restriction of $\mathbf{1}^{(S(n))}$ to $[n]$ is $\mathbf{1}^{(n)}$. Hence (S1), used first in its recursion part and then in its restriction part, gives

Step 2: claim 2. Note first that $p<q$ makes $q\le p$ false: $p<q$ gives $p\le q$ by (O1), so $q\le p$ would give $p=q$ by (O2), contradicting (O3).

Fix $m\in\mathbb{N}$ and let $A$ be the set of those $n\in\mathbb{N}$ such that either $n\le m$, or else both $m<n$ and $\sigma(m)+1\le\sigma(n)$. By (O4) we have $1\le m$, so $1\in A$.

Let $n\in A$. If $S(n)\le m$, then $S(n)\in A$. Otherwise $m<S(n)$, because by (O3) the alternatives $S(n)<m$ and $S(n)=m$ would each give $S(n)\le m$ by (O1). There are two cases.

Case $n\le m$. From $m<S(n)$ we get $m\le S(n)$ by (O1) and $m\ne S(n)$ by (O3), so (O5) gives $m\le n$ and hence $n=m$ by (O2). Step 1 then gives $\sigma(S(n))=\sigma(n)+1=\sigma(m)+1$.

Case $m<n$ and $\sigma(m)+1\le\sigma(n)$. Step 1 and step 0(b) give $\sigma(n)\le\sigma(n)+1=\sigma(S(n))$, so transitivity gives $\sigma(m)+1\le\sigma(S(n))$.

In both cases $m<S(n)$ and $\sigma(m)+1\le\sigma(S(n))$, so $S(n)\in A$. By Principle of Induction for the Natural Numbers, $A=\mathbb{N}$.

Now let $m<n$. Then $n\le m$ is false, so $\sigma(m)+1\le\sigma(n)$. Step 0(b) gives $\sigma(m)\le\sigma(m)+1$, hence $\sigma(m)\le\sigma(n)$ by transitivity; and $\sigma(m)=\sigma(n)$ would give $\sigma(m)+1\le\sigma(m)$, which step 0(b) excludes.

Step 3: claim 3. Let $\sigma(m)=\sigma(n)$. By (O3) exactly one of $m<n$, $m=n$, $n<m$ holds, and claim 2 excludes the first and the third. Hence $m=n$.