In this file we define the quotient of pre-games by the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤ p, and construct an instance add_comm_group game, as well as an instance partial_order game (although note carefully the warning that the < field in this instance is not the usual relation on combinatorial games).
The type of combinatorial games. In ZFC, a combinatorial game is constructed from two sets of combinatorial games that have been constructed at an earlier stage. To do this in type theory, we say that a combinatorial pre-game is built inductively from two families of combinatorial games indexed over any type in Type u. The resulting type pgame.{u} lives in Type (u+1), reflecting that it is a proper class in ZFC. A combinatorial game is then constructed by quotienting by the equivalence x ≈ y ↔ x ≤ y ∧ y ≤ x.
The relation x ≤ y on games.
The relation x < y on games.
The negation of {L | R} is {-R | -L}.
The sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.
The < operation provided by this partial order is not the usual < on games!
The < operation provided by this ordered_comm_group is not the usual < on games!