Birthday of dyadic rationals

We prove that a surreal number has a finite birthday iff it's a dyadic number.

@[simp]

theorem Game.birthday_ratCast (x : ℚ) : (↑x).birthday = (↑x).birthday

theorem Surreal.birthday_dyadic_lt_omega0 (x : Dyadic) : (↑↑x).birthday < NatOrdinal.of Ordinal.omega0

theorem Surreal.birthday_lt_omega0_iff {x : Surreal} : x.birthday < NatOrdinal.of Ordinal.omega0 ↔ x ∈ Set.range fun (x : Dyadic) => ↑↑x