Squaring is monotone on the nonnegatives

The difference factors as $b^2-a^2=(b-a)(b+a)$.

If $a,b\ge 0$ and $a<b$, then $b>0$, so $b+a>0$ by [L2], and $b-a>0$; by [L1] with $s=b+a$ and $t=b-a$, $(b-a)(b+a)>0$, i.e. $a^2<b^2$.

If $a,b\ge 0$ and $a^2<b^2$, then $b^2-a^2>0$, so $a,b$ are not both zero and $b+a>0$ by [L2]; by [L1] with $s=b+a$, from $(b-a)(b+a)=b^2-a^2>0$ we get $b-a>0$, i.e. $a<b$.

Hence for $a,b\ge 0$, $a<b⟺a^2<b^2$.

The $\le$ form follows by trichotomy: for $a,b\ge 0$, applying step 3.1 to the nonnegatives $b,a$ gives $a\le b⟺\mathrm{\neg }(b<a)⟺\mathrm{\neg }(b^2<a^2)⟺a^2\le b^2$.

For arbitrary $a,b$, [L3] gives $\mathrm{\mid }a\mathrm{\mid },\mathrm{\mid }b\mathrm{\mid }\ge 0$ with $\mathrm{\mid }a{\mathrm{\mid }}^2=a^2$ and $\mathrm{\mid }b{\mathrm{\mid }}^2=b^2$; applying step 3.1 to $\mathrm{\mid }a\mathrm{\mid },\mathrm{\mid }b\mathrm{\mid }$ yields $a^2<b^2⟺\mathrm{\mid }a{\mathrm{\mid }}^2<\mathrm{\mid }b{\mathrm{\mid }}^2⟺\mathrm{\mid }a\mathrm{\mid }<\mathrm{\mid }b\mathrm{\mid }$.