We have $$\operatorname{mex} S=\min \{n \in \mathbb{N} \mid n \notin S\},a \oplus b=\operatorname{mex}\{a' \oplus b ; a \oplus b', \forall a', b'\in \mathbb{N}: a'<a, b'<b\},$$ and $$a \otimes b=\operatorname{mex}\{(a' \oplus b) \oplus (a \otimes b') \oplus (a' \otimes b') \mid a',b' \in \mathbb{N}, a'<a, b'<b\}.$$ Let $c \in \mathbb{N}^*$, prove that there exists a unique number $d \in \mathbb{N}$ such that $c \otimes d = 1$.
The operation $\otimes$ is called the nim multiplication. I have proven its commutative, associative, and distributive properties with addition. I am currently proving its existence of an inverse. In the book "On Numbers and Games" by John H. Conway, on page 56, there is a mention of the formula for the inverse, but there is no mention of the proof, stating similarly to chapter 1. I have revisited chapter 1 but gained no insight.
Following Conway's convention, instead of using $\oplus, \otimes$, and $\oslash$ for nimber operations, I will just use the ordinary $+,\cdot,$ and $\frac{x}y$.
We will need to use the fact that nimber multiplication has no zero divisors. That is, if $a$ and $b$ are nonzero nimbers, then $ab\neq 0$. To see this, note that $ab\neq a'b+ab'+a'b'$ for all $a'<a$ and $b'<b$, and take $a'=b'=0$.
In ONAG, Conway gives the following inductive definition for the nim multiplicative inverse. When $x\neq 0$ is a nimber, $$ \frac1x=\text{mex }(Y),\text{ where }\\ Y=\left\{0,\frac{1+(x+x')\cdot y'}{x'} \mid 1\le x'<x ,y'\in Y\right\} $$ The way that I wrote it, $Y$ is circularly defined in terms of itself. To be rigorous, define a sequence of sets $Y_0,Y_1,Y_2,\dots$ inductively as follows: $$ \begin{align} Y_0&=\{0\}\\ Y_{n+1}&=\left\{\frac{1+(x+x')\cdot y'}{x'} \mid 1\le x'<x,y'\in Y_n\right\} \qquad (n\ge 0) \end{align} $$ We then define $Y=\bigcup_{n=0}^\infty Y_n$.
Proof: If $y'=0$, then obviously $xy'=0\neq 1$. Otherwise, since $y'\in Y_n$ for some $n\ge 1$, then we know that $$y'=\frac{1+(x+x')y''}{x'}$$ for some $x'<x$ and some $y''\in Y_{n-1}$. We can rewrite this equation as $$ (1+xy')=(1+xy'')\cdot (x+x')\cdot \frac1{x'} $$ Now, by induction on $n$, we know that $xy''\neq 1$, so that $1+xy''\neq 0$. Since $x'<x$, we have $x'+x\neq 0$. Finally, applying the formula for $\frac1x$ inductively to $x'$, we know that $0$ is an excludant for $\frac1{x'}$, so $\frac1{x'}\neq 0$. All three factors are nonzero, so the fact that nimber multiplication has no zero divisors implies that $1+x'y\neq 0$, so $xy'\neq 1$.
$\tag*{$\square$}$
Proof: Recalling that $$xy=\operatorname{mex}P, \text{ where }P=\{x'y+xy'+x'y'\mid x'<x, y'<y\},$$ we just need to show $\operatorname{mex} P=1$, which is equivalent to $0\in P$ and $1\notin P$. To see that $0\in P$, simply take $x'=0$ and $y'=0$ in the definition of $P$.
We must show $xy'+x'y+x'y'\neq 1$ for all $x'<x$ and $y'<y$. In the case where $x'=0$, this is equivalent to showing $xy'\neq 1$ for all $y' < y$, which was handled by the Lemma. From now on, assume $x'\neq 0$. In this case, we can write $$ x'y+xy'+x'y'=1+x'y+x'\cdot \frac{1+(x+x')y'}{x'} $$ Say that $y'\in Y_n$. Letting $y''=\frac{1+(x+x')y'}{x'}$, by definition we have $y''\in Y_{n+1}$. The above becomes $$ x'y+xy'+x'y'=1+x'y + x'\cdot y''=1+x'(y+y'') $$ Now, since $y=\operatorname{mex} Y$ and $y''\in Y$, it follows $y\neq y''$, which implies that $y+y''\neq 0$. Since there are no zero-divisors, and since $x'\neq 0$, we conclude $1+x'(y+y'')\neq 1$. This proves that $x'y+xy'+x'y'\neq 1$ for all $x'<x$ and $y'<y$, as required.
$\tag*{$\square$}$