Nonnegativity of Squares in an Ordered Field

Let $F$ together with $\le$ be an ordered field, with additive identity $0$. For $t\in F$ write $t^{2}$ for $t\cdot t$, and write $|t|$ for the absolute value of $t$.

Let $t\in F$. Then the following hold.

1. (Agreement with the absolute value) $t^{2}=|t|^{2}$.

2. (Nonnegativity) $0\le t^{2}$.