Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $\omega$ and $0$ be as in The Class Omega of Natural Numbers with Zero §omega and The Class Omega of Natural Numbers with Zero §zero, let $S(x)$ denote the successor of a set $x$, let $+$ be the addition on $\omega$, and let $\le$ and $<$ be the order and the strict order on $\omega$. Let $k,m,n\in\omega$.

¶ $m+0=m$ and $0+m=m$.

¶ $m+S(n)=S(m+n)$ and $S(m)+n=S(m+n)$; in particular $S(n)=n+S(0)$.

¶ $(k+m)+n=k+(m+n)$.

¶ $m+n=n+m$.

¶ If $k+m=k+n$, then $m=n$.

¶ $m<n$ if and only if $k+m<k+n$, and $m\le n$ if and only if $k+m\le k+n$.

¶ $m\le n$ if and only if there is $j\in\omega$ with $m+j=n$.

¶ If $m+n=0$, then $m=0$ and $n=0$.