English
Nimber multiplication distributes over addition on the left: a*(b+c) = a*b + a*c.
Русский
Умножение Nimber распределяется над сложением слева: a*(b+c) = a*b + a*c.
LaTeX
$$$ a \cdot (b + c) = a \cdot b + a \cdot c $$$
Lean4
protected theorem mul_add (a b c : Nimber) : a * (b + c) = a * b + a * c :=
by
apply le_antisymm
· refine mul_le_of_forall_ne fun a' ha x hx ↦ ?_
obtain (⟨b', h, rfl⟩ | ⟨c', h, rfl⟩) := exists_of_lt_add hx <;>
rw [Nimber.mul_add a', Nimber.mul_add a, Nimber.mul_add a']
on_goal 1 => rw [← add_ne_add_left (a * c)]
on_goal 2 => rw [← add_ne_add_left (a * b)]
all_goals
abel_nf
simp only [two_zsmul, zero_add]
rw [← add_assoc]
exact mul_ne_of_lt _ ha _ h
· apply add_le_of_forall_ne <;> (intro x' hx'; obtain ⟨x, hx, y, hy, rfl⟩ := exists_of_lt_mul hx')
· obtain h | h | h := lt_trichotomy (y + c) (b + c)
· have H := mul_ne_of_lt _ hx _ h
rw [Nimber.mul_add x, Nimber.mul_add a, Nimber.mul_add x] at H
abel_nf at H ⊢
simpa only [two_zsmul, zero_add] using H
· exact (hy.ne <| add_left_injective _ h).elim
· obtain ⟨z, hz, hz'⟩ | ⟨c', hc, hc'⟩ := exists_of_lt_add h
· exact ((hz.trans hy).ne <| add_left_injective _ hz').elim
· have := add_eq_iff_eq_add.1 hc'
have H := mul_ne_of_lt _ hx _ hc
rw [← hc', Nimber.mul_add a y c', ← add_ne_add_left (a * y), ← add_ne_add_left (a * c), ←
add_ne_add_left (a * c'), ← add_eq_iff_eq_add.2 hc', Nimber.mul_add x, Nimber.mul_add x]
abel_nf at H ⊢
simpa only [two_zsmul, add_zero, zero_add] using H
· obtain h | h | h := lt_trichotomy (b + y) (b + c)
· have H := mul_ne_of_lt _ hx _ h
rw [Nimber.mul_add x, Nimber.mul_add a, Nimber.mul_add x] at H
abel_nf at H ⊢
simpa only [two_zsmul, zero_add] using H
· exact (hy.ne <| add_right_injective _ h).elim
· obtain ⟨b', hb, hb'⟩ | ⟨z, hz, hz'⟩ := exists_of_lt_add h
· have H := mul_ne_of_lt _ hx _ hb
have hb'' := add_eq_iff_eq_add.2 (add_comm b c ▸ hb')
rw [← hb', Nimber.mul_add a b', ← add_ne_add_left (a * y), ← add_ne_add_left (a * b), ←
add_ne_add_left (a * b'), ← hb'', Nimber.mul_add x, Nimber.mul_add x]
abel_nf at H ⊢
simpa only [two_zsmul, add_zero, zero_add] using H
· exact ((hz.trans hy).ne <| add_right_injective _ hz').elim
termination_by (a, b, c)
