English
Addition in Nimbers is associative (protecting the property).
Русский
Сложение Nimbers ассоциативно (защищенная свойство).
LaTeX
$$$\\\\forall a\\\\ b\\\\ c: \\\\mathrm{Nimber},\\\\ a + b + c = a + (b + c).$$$
Lean4
protected theorem add_assoc (a b c : Nimber) : a + b + c = a + (b + c) :=
by
apply le_antisymm <;> apply add_le_of_forall_ne <;> intro x hx <;>
try obtain ⟨y, hy, rfl⟩ | ⟨y, hy, rfl⟩ := exists_of_lt_add hx
on_goal 1 => rw [Nimber.add_assoc y, add_ne_add_left]
on_goal 2 => rw [Nimber.add_assoc _ y, add_ne_add_right, add_ne_add_left]
on_goal 3 => rw [Nimber.add_assoc _ _ x, add_ne_add_right, add_ne_add_right]
on_goal 4 => rw [← Nimber.add_assoc x, add_ne_add_left, add_ne_add_left]
on_goal 5 => rw [← Nimber.add_assoc _ y, add_ne_add_left, add_ne_add_right]
on_goal 6 => rw [← Nimber.add_assoc _ _ y, add_ne_add_right]
all_goals apply ne_of_lt; assumption
termination_by (a, b, c)
