English
Addition in Nimbers is associative: (a + b) + c = a + (b + c).
Русский
Сложение Nimbers ассоциативно: (a + b) + c = a + (b + c).
LaTeX
$$$\\\\forall a\\\\ b\\\\ c: \\\\mathrm{Nimber},\\\\ (a + b) + c = a + (b + c).$$$
Lean4
theorem add_eq_zero {a b : Nimber} : a + b = 0 ↔ a = b :=
by
constructor <;> intro hab
· obtain h | rfl | h := lt_trichotomy a b
· have ha : a + a = 0 := add_eq_zero.2 rfl
rwa [← ha, add_right_inj, eq_comm] at hab
· rfl
· have hb : b + b = 0 := add_eq_zero.2 rfl
rwa [← hb, add_left_inj] at hab
· rw [← Nimber.le_zero]
apply add_le_of_forall_ne <;> simp_rw [ne_eq] <;> intro x hx
· rw [add_eq_zero, ← hab]
exact hx.ne
· rw [add_eq_zero, hab]
exact hx.ne'
termination_by (a, b)
