refactor(set_theory/game/ordinal): Improve API (#13878)
We change our former equivalence `o.out.α ≃ o.to_pgame.left_moves` to an equivalence `{o' // o' < o} ≃ o.to_pgame.left_moves`. This makes two proofs much simpler.
We also add a simple missing lemma, `to_pgame_equiv_iff`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
