English
If a + b + c ≠ 0, then exactly one of b + c < a, c + a < b, a + b < c holds.
Русский
Если a + b + c не равно нулю, то выполняется ровно одно из b + c < a, c + a < b, a + b < c.
LaTeX
$$$\\\\forall {a\\\\ b\\\\ c: \\\\mathrm{Nimber}},\\\\ (a + b + c) \\\\neq 0 \\\\Rightarrow \\\\bigl( b + c < a \\\\lor \\\\ c + a < b \\\\lor \\\\ a + b < c \\\\bigr).$$$
Lean4
theorem add_trichotomy {a b c : Nimber} (h : a + b + c ≠ 0) : b + c < a ∨ c + a < b ∨ a + b < c :=
by
rw [← Nimber.pos_iff_ne_zero] at h
obtain ⟨x, hx, hx'⟩ | ⟨x, hx, hx'⟩ := exists_of_lt_add h <;> rw [add_eq_zero] at hx'
· obtain ⟨x, hx, hx'⟩ | ⟨x, hx, hx'⟩ := exists_of_lt_add (hx' ▸ hx)
· rw [← hx', add_comm, add_cancel_right]
exact Or.inl hx
· rw [← hx', add_comm a, add_cancel_right]
exact Or.inr <| Or.inl hx
· rw [← hx'] at hx
exact Or.inr <| Or.inr hx
