feat(set_theory/surreal): add add_monoid instance (#7228)
This PR is a part of a project for putting ordered abelian group structure on surreal numbers.
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Surreal.20numbers/near/234694758)
We construct add_monoid instance for surreal numbers.
The "term_type" proofs suggested on the above Zulip thread are not working nicely as Lean is unable to infer the type of the setoid.
