Elementary Arithmetic in an Ordered Field

Let $F$ be an \reftext{def:ordered-field-c54-2026b}{ordered field}, with the additive identity $0$, multiplicative identity $1$, additive inverses $-x$ and multiplicative inverses $x^{-1}$ of a \reftext{def:field-c54-2026b}{field}, and with its order $\le$; write $x-y=x+(-y)$. Let $a,b,x,y\in F$. Then the following hold.

\textbf{1. (The unit is nonnegative)} $0\le 1$.

\textbf{2. (Sums)} If $0\le a$ and $0\le b$, then $0\le a+b$.

\textbf{3. (Translation)} $x\le y$ holds if and only if $0\le y-x$.

\textbf{4. (Inverses)} If $0\le a$ and $a\ne 0$, then $a^{-1}\ne 0$ and $0\le a^{-1}$.

\textbf{5. (Multiplying by a nonnegative element)} If $x\le y$ and $0\le a$, then $ax\le ay$.