mathlib

b8d8a5e4 - refactor(set_theory/game/*): Fix bad notation `<` on (pre-)games (#13963)

refactor(set_theory/game/*): Fix bad notation `<` on (pre-)games (#13963) Our current definition for `<` on pre-games is, in the wider mathematical literature, referred to as `⧏` (less or fuzzy to). Conversely, what's usually referred to by `<` coincides with the relation we get from `preorder pgame` (which the current API avoids using at all). We rename `<` to `⧏`, and add the basic API for both the new `<` and `⧏` relations. This allows us to define new instances on `pgame` and `game` that we couldn't before. We also take the opportunity to add some basic API on the fuzzy relation `∥`. See the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Surreal.20numbers/near/281094687).