Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field

Let $F$ together with $\le$ be an ordered field, with additive identity $0$, and for $s,t\in F$ let $s<t$ denote the associated strict order, that is, $s\le t$ together with $s\ne t$. For $\gamma\in F$ write $\gamma^{2}$ for $\gamma\cdot\gamma$.

Let $\alpha,\beta\in F$ satisfy $0\le\alpha$ and $0\le\beta$. Then the following hold.

1. (Strict form) $\alpha<\beta$ if and only if $\alpha^{2}<\beta^{2}$.

2. (Weak form) $\alpha\le\beta$ if and only if $\alpha^{2}\le\beta^{2}$.

3. (Equality form) $\alpha=\beta$ if and only if $\alpha^{2}=\beta^{2}$.