English
Two nimbers Nim(o1) and Nim(o2) are equivalent to zero iff o1 = o2; i.e., Nim(o1) + Nim(o2) ≈ 0 ⇔ o1 = o2.
Русский
Две нимбер-игры Nim(o1) и Nim(o2) эквивалентны нулю тогда и только тогда, когда o1 = o2; то есть Nim(o1) + Nim(o2) ≈ 0 ⇔ o1 = o2.
LaTeX
$$$ (\mathrm{nim}(o_1) + \mathrm{nim}(o_2) \approx 0) \;\iff\; o_1 = o_2. $$$
Lean4
@[simp]
theorem nim_add_equiv_zero_iff (o₁ o₂ : Ordinal) : (nim o₁ + nim o₂ ≈ 0) ↔ o₁ = o₂ :=
by
constructor
· refine not_imp_not.1 fun hne : _ ≠ _ => (Impartial.not_equiv_zero_iff (nim o₁ + nim o₂)).2 ?_
wlog h : o₁ < o₂
· exact (fuzzy_congr_left add_comm_equiv).1 (this _ _ hne.symm (hne.lt_or_gt.resolve_left h))
rw [Impartial.fuzzy_zero_iff_gf, zero_lf_le]
use toLeftMovesAdd (Sum.inr <| toLeftMovesNim ⟨_, h⟩)
· simpa using (Impartial.add_self (nim o₁)).2
· rintro rfl
exact Impartial.add_self (nim o₁)
