EDB — 28R

We will use some properties left for exercise.

• If $n\le m$, by definition $m=n+h$, then $n+k\le m+k$ because $m+k=n+h+k$ (note that we are using associativity). If $n+k\le m+k$ let then $j$ the only natural number such that $n+k+j=m+k$ but then $n+j=m$ by cancellation [27V]↺↻.

• If $n\le m$ then $m=n+h$ therefore $m\times k=n\times k+h\times k$ so $n\times k\le m\times k$. Vice versa let $k\ne 0$ and $n\times k\le m\times k$ i.e. $n\times k+j=m\times k$: divide $j$ by $k$ using the division [28J]↺↻, we write $j=q\times k+r$ therefore for associativity $(n+q)\times k+r=m\times k$ but for the uniqueness of the division $r=0$; eventually collecting $(n+q)\times k=m\times k$ and using [28M]↺↻ we conclude that $(n+q)=m$.