English
If b ≠ 1 and b is additive principal, then a*b is additive principal for all a.
Русский
Если b ≠ 1 и b принципиален для сложения, то для любого a число a*b тоже принципиально для сложения.
LaTeX
$$$(hb_1 : b \neq 1) \land Principal(\cdot + \cdot, b) \Rightarrow Principal(\cdot + \cdot, a*b).$$$
Lean4
theorem principal_add_mul_of_principal_add (a : Ordinal.{u}) {b : Ordinal.{u}} (hb₁ : b ≠ 1)
(hb : Principal (· + ·) b) : Principal (· + ·) (a * b) :=
by
rcases eq_zero_or_pos a with (rfl | _)
· rw [zero_mul]
exact principal_zero
· rcases eq_zero_or_pos b with (rfl | hb₁')
· rw [mul_zero]
exact principal_zero
· rw [← succ_le_iff, succ_zero] at hb₁'
intro c d hc hd
rw [lt_mul_iff_of_isSuccLimit (isSuccLimit_of_principal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
rcases hc with ⟨x, hx, hx'⟩
rcases hd with ⟨y, hy, hy'⟩
use x + y, hb hx hy
rw [mul_add]
exact Left.add_lt_add hx' hy'
