Prove every small ordered field embeds in `Surreal`

[vihdzp]

I believe there's three results we have to prove for this:

• Surreal is isomorphic to real Hahn series over itself.
• Every small linear ordered group embeds in Surreal. This can be done via a transfinite induction argument; I'm not aware of an easier way to prove this.
• Every linear ordered field $K$ embeds in its Hahn group $\mathbb R[[X^\Gamma]]$ (where $\Gamma$ is the linear group of Archimedean classes). This is a field version of the Hahn embedding theorem (though we don't yet have the group version in Mathlib!)

Then, to embed an arbitrary (small) field $K$ into the surreals, it suffices to embed its Archimedean classes as $\Gamma'$, giving us the full embedding $$K \to \mathbb R[[X^\Gamma]] \to \mathbb R[[X^{\Gamma'}]] \to \mathrm{No}$$.