Elementary Arithmetic in an Ordered Field

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

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

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

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

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

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