feat(set_theory/game/basic): Basic lemmas on `inv` (#13840)
Note that we've redefined `inv` so that `inv x = 0` when `x ≈ 0`. This is because, in order to lift it to an operation on surreals, we need to prove that equivalent numeric games give equivalent numeric values, and this isn't the case otherwise.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Mauricio Collares <mauricio@collares.org>
