surreal multiplication

Stream: mathlib4

[Ted Hwa]

In #14044 I ported from Lean 3 to Lean 4 the surreal multiplication proofs that were in this old mathlib3 branch. It looks like the proofs were completed but never ported to Lean 4. Tagging original authors @Violeta Hernández @Junyan Xu

[Violeta Hernández]

Thanks for reviving this! It's been a while since I touched Lean, but I'm free for the summer, so feel free to tag me for any relevant PR reviews