Proof of Conway's "Simplicity Rule" for Surreal Numbers A "number" in the sense of Combinatorial Game Theory is a game
 $G = \{ a,b,c,\dots | \; d,e,f,\dots \}$ such that $a,b,c < d,e,f$.  Then our game is between the left and right options:
$$  a,b,c <  G < d,e,f $$
However, we still don't know which number we are dealing with until we invoke his Simplicity Rule

If there's any number that fits, it's the simplest number that fits.

At this point, we don't necessarily know that all finite games should have denominators which are power of $2$, but it's true.  Instead we get 4 rules and  a fuzzy notion of "simplicity":


*

*$0 = \{ | \}$

*$n+1 = \{ n| \}$

*$-n-1 = \{ | -n \}$

*$\tfrac{2p+1}{2^{q+1}} = \left\{\tfrac{p}{2^q}  | \tfrac{p+1}{2^q} \right\} $


The numbers we construct kind of resemble the notches of a ruler

It is known these games generalize Dedekind cut construction of the real numbers from the Rationals.  However $\mathbb{Q}$ hasn't been constructed yet... not even $\mathbb{Z}[\tfrac{1}{2}]$.  How do we prove these simplicity rules?
 A: The definition of number and integers
The definition of "number" in Combinatorial Game Theory is not "a game $G$ such that every right option is greater than every left option". For example, with $*\cong\{0|0\}$ and $\uparrow\cong\{0|*\}$, the game $\{0|\uparrow\}$ satisfies your condition (as $\uparrow>0$), but is not a number.
One definition of "number" could be Definition A: "a game $G$ such that all options are numbers and every right option is greater than every left option", but that's stronger than necessary.
I prefer defining "number" as Definition B: "a game $G$ such that all options are numbers and no right option is less than or equal to any left option" and then proving it satisfies the stronger definition.
Note that the natural numbers games you defined (e.g. $0=\{|\}$,$1=\{0|\}$,...) are numbers in the sense of either definition by an immediate induction: their option is a number by induction and they don't have a right option to violate the inequality clause.
Also note that the negative of a number (by either definition) is automatically a number (by the same definition), so that gives us the rest of the integers. I'll talk about the dyadic fractions (rationals whose denominator is a power of 2) later.

Simplicity Rule
The simplicity rule will take some work to reach. I'll use definition B in what follows and prove that numbers satisfy definition A along the way.
Lemma 1: Numbers are between their options
Proof: We'll prove that a number $G$ is greater than all of its left options; the proof that it's less than all of its right options is exactly analogous. Let $G$ be a number, and assume, as an inductive hypothesis, that lemma 1 is true for all of the options of $G$. Let $G^L$ be a left option of $G$. Then to check $G>G^L$, we need to see that Left can always win $G-G^L$. If Left goes first, she can just move to $G^L-G^L=0$ and win. If Right moves first to some $G^R-G^L$, then since $G$ is a Number, we know that $G^R\nleq G^L$ (by definition B) so that Left wins $G^R-G^L$ going first. Finally, if Right moves first to some $G+\left(-G^L\right)^R=G-\left(G^{LL}\right)$ (by this I mean that a right option of $-G^L$ is the negative of a left option of $G^L$), then Left can win by moving to $G^L-G^{LL}>0$ (inductive hypothesis applied to $G^L$).  $\square$
Corollary 1
Now we can see that definition B implies definition A. By lemma 1, which only assumed definition B, we have $G^L<G$ for all left options, and $G<G^R$ for all right options. By transitivity of $<$, we can conclude that for all pairs of options, $G^R>G^L$, as desired. $\square$
Lemma 2: Numbers are closed under sum
Proof: Let $G$ and $H$ be numbers. Recall that $G+H=\left\{\mathcal{G}^L+H,G+\mathcal{H}^L\left|\mathcal{G}^R+H,G+\mathcal{H}^R\right.\right\}$. Assume, for sake of contradiction, that some right option of $G+H$ is less than or equal to a left option. Case I: Suppose $G^R+H\le G^L+H$. Then $G^R\le G^L$ which is impossible since $G$ is a number. Case II: Suppose $G^R+H\le G+H^L$. By lemma 1, $H^L<H$, so $G+H^L<G+H$. Analogously, $G+H<G^R+H$. But then we have $G+H<G^R+H\le G+H^L<G+H$, which is a contradiction. Cases III and IV are analogous. $\square$
Lemma 3: Numbers are pairwise comparable
Proof: If $G$ and $H$ are numbers, then $-H$ is a number by the remark in the first section, and hence $G-H$ is a number by lemma 2. Since $G$ being incomparable with $H$ is equivalent to $G-H$ being a first-player win (an $\mathcal{N}$-position), it suffices to show that no number is a first-player win. Suppose for sake of contradiction that a number $G$ is a win for the first player. Then choose winning moves $G^L$ and $G^R$. To be winning moves, we must have $G^L\ge0$ and $G^R\le0$, so that $G^R\le G^L$, which is a contradiction. $\square$.
Lemma 4: Proto-Simplicity
Definition: A game $H$ "fits" for a game $G$ if $\mathcal{G}^L\ngeq H\ngeq\mathcal{G}^R$; that is, $H$ fits for $G$ if $H$ lies strictly between (or is incomparable to) the left and right options of $G$. With this definition, lemma 1 implies that a number fits for itself.
Lemma Statement: If $H$ is a number, and $H$ fits for $G$ but none of $H$'s options fit for $G$, then $G=H$.
Proof: We need to show that the second player has a winning strategy on $G-H$. If Left makes the first move to $G^L-H$, then since $H$ fits for $G$, $G^L-H\ngeq0$ and Right can win. Now suppose Left makes the first move to $G-\left(H^R\right)$. Since none of $H$'s options fit for $G$, $H^R$ doesn't fit for $G$, and there must be a witnessing (in)equality of the form $G^L\geq H^R$ or $G^R\leq H^R$. By lemma 1, $H^R>H$, and since $H$ fits for $G$, $G^L<H<H^R$, so that $G^L\geq H^R$ would be impossible. Therefore, there must be an option $G^R\leq H^R$. Thus, Right can win by moving from $G-\left(H^R\right)$ to $G^R-\left(H^R\right)\le0$. The two cases in which Right makes the first move are analogous. $\square$
Lemma 5: Simplest fitting numbers
Statement: If $G$ is a game, and any number fits for $G$, then there is a lowest birthday among birthdays of numbers $H$ that fit for $G$.
Proof: This follows immediately from the fact that the ordinals are well-ordered. $\square$
Theorem: Simplicity Rule
Statement: If $G$ is a game, and any number fits for $G$, then $G$ is equal to any minimal-birthday fitting-number.
Proof: If $H$ has the lowest birthday of any fitting number, no option of $H$ could fit, so the result follows from lemma 4. $\square$
Corollary 2
In particular, if $G$ is equal to a number $H$, lemma 1 shows that $H$ fits for itself (and hence $H$ fits for $G=H$), so $G$ is equal to any minimal-birthday fitting-number by the simplicity rule. $\square$
Note that the simplicity rule doesn't say anything about uniqueness: the number $\omega\cong\{0,1,2,3,\ldots|\}=\{0,2,4,\ldots|\}$, but both forms have minimal birthday $\omega$ (the ordinal).

All finite-birthday numbers are equal to a dyadic
Proof: Suppose that $G$ is a number with finite-birthday and all numbers of earlier birthday are equal to a dyadic. Then $G$ has finitely many options, all dyadic. Since the dyadics (and in fact all numbers, by lemma 3) are pairwise comparable, we can assume $G$ is in canonical form with at most one left option and at most one right option, both necessarily dyadic. If an integer fits, then by applying lemma 4 and induction, $G$ is equal to the smallest absolute value integer that fits. If no integer fits, then there's a unique dyadic of smallest denominator that fits, and $G$ is equal to that.

How do we get $\mathbb Q$ and $\mathbb R$
You can get elements of $\mathbb R$ that are not-dyadic on day $\omega$ by using Dedekind cuts with dyadics. In other words, if $r$ is a real that is not dyadic, then $r=\left\{\text{dyadics}<r\left|\text{dyadics}>r\right.\right\}$.
There's also a nice implicit definition of the reals: a number $G$ is real if $G$ is bounded by integers ($-n<G<n$ for some natural $n$) and $G$ is "simply approximated by dyadics" in the sense that $G=\{G-q|G+q\}$ where $q$ ranges over the positive dyadics.

Some of this was based on old blog posts I made as I was working through Winning Ways/On Numbers and Games, but a couple tricky bits are based on Aaron N. Siegel's Combinatorial Game Theory.
A: The four rules are defining what we mean by strings that look like integers and dyadic fractions.  Conway's system has some axioms which only use a few characters like $\{, \},$ and $|$.  From those we can create $\{ | \}$ and see that it meets the definition of number.  We then (per the first rule) give it a name "$0$".  In theory, we could give it any name we like, say "Alphie", but giving it the name zero tends to imply it will work like the real number zero we are accustomed to.  Even using the $n$ in the definitions rests on our understanding of the natural numbers and he owes us that $2$ in his definition will behave like the $2$ we know and love.  We can unpack the definition of $2$ and find that it is a name for $\Bigl \{\bigl\{\{ | \}|\bigr \}|\Bigr\}$.  This is similar to Peano Arithmetic where $0$ is part of the language and we define $2=S(S(0))$ to shorten presentations.  It would be perverse to define "$3$" as $S(S(0))$ because it wouldn't work right.  We need to prove the Simplicity Rule, which is independent of these definitions.  We have defined $\frac 12=\{0|1\}$.  Now we need to prove that $\{0|x\}=\frac 12$ for any number $\frac 12\lt x \le 1$.  Using his game theory formulation, we need to show that $\{0|x\}+\{0|x\}+\{|0\}=0$, in that whoever moves first loses.
