Inductive hypothesis in surreal multiplication proof I'm having a hard time reading through Theorem 8 of On Numbers and Games. To prove that the multiplication of numeric games is a number, Conway sets up a simultaneous (Conway) induction with three statements:

*

*If $x$, $y$ are numbers, then $xy$ is a number.

*If $x_1=x_2$ then $x_1y=x_2y$.

*If $x_1< x_2$ and $y_1< y_2$ then $x_1y_2+x_2y_1<x_1y_1+x_2y_2$.

Immediately striking is that these statements all use different variables. Conway doesn't seem to mind this, and just uses any of these statements in the proof of the others. This begs the question: what is the inductive hypothesis?
I've seen an alternate proof of the well-definedness of multiplication, but I'm wondering if this inductive argument can be salvaged.
 A: Junyan Xu and I have managed to produce a slightly simplified version of Schliecher–Stoll's argument that uses induction more directly (instead of relying on the ad-hoc notion of game depth). For posterity, and given the lack of proofs of this theorem available, I'm posting it here.
We prove the following two assertions simultaneously:

*

*If $x$ and $y$ are numbers, then $xy$ is a number.

*If $x_1$, $x_2$, $y$ are numbers, then

*

*If $x_1=x_2$, then $x_1y=x_2y$.

*If $x_1<x_2$, then for any left option $y^L$ and right option $y^R$ of $y$,

*

*$x_1y+x_2y^L<x_1y^L+x_2y$.

*$x_1y^R+x_2y<x_1y+x_2y^R$.





Perhaps unorthodoxly, we induct on the multisets of arguments $\{x,y\}$ and $\{x_1,x_2,y\}$ for these claims. More specifically, we consider the hydra game  on finite multisets. At each step, we can replace an element of our finite multiset with finitely many elements comparing as lesser to the removed element under some well-founded relation (in this case, game subsequency). We write $S\prec T$ when $S$ can be reached from $T$ after finitely many steps of the hydra game.
It turns out that $\prec$ is well-founded (as is shown in the linked post), which means that we may induct on it. That is, if we prove that our simultaneous assertion follows from lesser multisets of arguments, we're done.
The proof of this statement and the necessary calculations exactly follow those from Schleicher–Stoll, modulo some variable renames. It can be (easily but tediously) verified that in all of our 36 applications of the inductive hypothesis, the multisets of arguments we call it on are indeed lesser under $\prec$.
