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, -y ≤ a) : ¬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, -z ≤ a) : ⧾a ≤ 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.tiny_toIGame_birthday_lt {x : IGame} (hx : 0 < x) : ⧾NatOrdinal.toIGame x.birthday < x

theorem IGame.tiny_lt_of_toIGame_birthday_le {x : IGame} (hx : 0 < x) {o : IGame} (ho : NatOrdinal.toIGame x.birthday ≤ o) : ⧾o < x

theorem IGame.fuzzy_tiny_of_birthday_le {x : IGame} (hx : x ‖ 0) {o : IGame} (ho : NatOrdinal.toIGame x.birthday ≤ o) : x ‖ ⧾o

theorem IGame.fuzzy_tiny_toIGame_birthday {x : IGame} (hx : x ‖ 0) : x ‖ ⧾NatOrdinal.toIGame x.birthday

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

theorem IGame.lt_miny_toIGame_of_birthday_le {x : IGame} (hx : x < 0) {o : NatOrdinal} (ho : x.birthday ≤ o) : x < ⧿NatOrdinal.toIGame o

theorem IGame.fuzzy_miny_of_birthday_le {x : IGame} (hx : x ‖ 0) {o : IGame} (ho : NatOrdinal.toIGame x.birthday ≤ o) : x ‖ ⧿o

theorem IGame.fuzzy_miny_toIGame_birthday {x : IGame} (hx : x ‖ 0) : x ‖ ⧿NatOrdinal.toIGame x.birthday

instance IGame.instDenselyOrdered : DenselyOrdered IGame

instance IGame.instDenselyOrderedGame : DenselyOrdered Game