feat(set_theory/game/pgame): Tweak `pgame.add` API (#13611)
We modify the API for `pgame.add` as follows:
- `left_moves_add` and `right_moves_add` are turned from type equivalences into type equalities.
- The former equivalences are prefixed with `to_` and inverted.
We also golf a few theorems and make some parameters explicit.
