We define the canonical map Ordinal → SetTheory.PGame, where every ordinal is mapped to the
game whose left set consists of all previous ordinals.
Ordinal → SetTheory.PGame
The map to surreals is defined in Ordinal.toSurreal.
Converts an ordinal into the corresponding pre-game.
Converts an ordinal less than o into a move for the PGame corresponding to o, and vice
0.to_pgame has the same moves as 0.
1.to_pgame has the same moves as 1.
The order embedding version of toPGame.
The sum of ordinals as games corresponds to natural addition of ordinals.