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$ or $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$, $x+y^R\leq x+z$, $x+y\leq x^L+z$, $x+y\leq x+z^L$,

and if we further suppose $y\geq z$, we deduce one of*

$x^R+y\leq x+y$, $x+y^R\leq x+y$, $x+z\leq x^L+z$, $x+z\leq x+z^L$,

All of which imply contradictions by cancellation.

I think I don't understand the step with the * correctly, because I think it would require the theorem itself, but that may be wrong.

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.

Does anyone here know about Conway's On numbers and games? Because I can't figure out what he does here on p18. what and how does he deduce when he says 'we deduce one of'? [the theorem in question][1] [1]: https://i.sstatic.net/SRLRO.jpg Because it feels a bit like he's using the statement we want to prove

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$ or $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$, $x+y^R\leq x+z$, $x+y\leq x^L+z$, $x+y\leq x+z^L$,

and if we further suppose $y\geq z$, we deduce one of*

$x^R+y\leq x+y$, $x+y^R\leq x+y$, $x+z\leq x^L+z$, $x+z\leq x+z^L$,

All of which imply contradictions by cancellation.

I think I don't understand the step with the * correctly, because I think it would require the theorem itself, but that may be wrong.