chore(set_theory/pgame): add protected (#9022)
Breaks #7843 into smaller PRs.
These lemmas about `pgame` conflict with the ones for `game` when used in `calc` mode proofs, which confuses Lean.
There is no way to use the lemmas for `game` (required for surreal numbers) without using `_root_` as `game` inherits these lemmas from its abelian group structure.
