Does anyone here know about Conway's On numbers and games? Because I can't figure out what he does here on p18. It feels a bit like he's using the statement we want to prove
I will type the proof below:
Theorem 5. We have $y\geq z$ iff $x+y\geq x+z$.
Proof. If $x+y\geq x+z$, we cannot have
$$x+y^R\leq x+z\quad\text{or}\quad x+y\leq x+z^L$$
and so by induction we cannot have $y^R\leq z$ or $y\leq z^L$ so that $y\geq z$.
Now supposing $x+y\ngeq x+z$ we must have one of
$$x^R+y\leq x+z,\quad x+y^R\leq x+z,\quad x+y\leq x^L+z,\quad x+y\leq x+z^L,$$
and if we further suppose $y\geq z$, we deduce one of
\begin{equation} \tag{$*$}\label{star} x^R+y\leq x+y,\quad x+y^R\leq x+y,\quad x+z\leq x^L+z,\quad x+z\leq x+z^L, \end{equation}
All of which imply contradictions by cancellation.
I think I don't understand the step \eqref{star} correctly, because I think it would require the theorem itself, but that may be wrong.
