feat(order/game_add): `sym2.game_add` (#18287)
We define `sym2.game_add`, which is a relation `sym2 α → sym2 α → Prop` which expresses that one pair may be obtained from the other by decreasing either entry. We add a basic API, and prove well-foundedness.
Pair: https://github.com/leanprover-community/mathlib4/pull/2532
