Games are densely ordered

We provide instances of DenselyOrdered for IGame and Game.

theorem IGame.tiny_lf_of_not_nonpos_of_forall_neg_le {x a : IGame} (hx : ¬x ≤ 0) (ha : ∀ y ∈ moves right x, -a ≤ y) : ¬x ≤ ⧾a

theorem IGame.tiny_le_of_pos_of_forall_neg_le {x a : IGame} (hx : 0 < x) (ha : ∀ y ∈ moves right x, ∀ z ∈ moves right y, -a ≤ z) : ⧾a ≤ x

theorem IGame.tiny_toIGame_birthday_lt {x : IGame} (hx : 0 < x) : ⧾NatOrdinal.toIGame x.birthday < x

theorem IGame.lf_miny_of_not_nonneg_of_forall_le {x a : IGame} (hx : ¬0 ≤ x) (ha : ∀ y ∈ moves left x, y ≤ a) : ¬⧿a ≤ x

theorem IGame.le_miny_of_neg_of_forall_le_neg {x a : IGame} (hx : x < 0) (ha : ∀ y ∈ moves left x, ∀ z ∈ moves left y, z ≤ a) : x ≤ ⧿a

theorem IGame.lt_miny_toIGame_birthday {x : IGame} (hx : x < 0) : x < ⧿NatOrdinal.toIGame x.birthday

instance IGame.instDenselyOrdered : DenselyOrdered IGame

instance IGame.instDenselyOrderedGame : DenselyOrdered Game