English
Equivalent reformulation of the strict nmul order using existential witnesses a' and b'.
Русский
Эквивалентная переработка строгого порядка nmul через существующие свидетели a' и b'.
LaTeX
$$$\\forall a,b,c \\in \\mathrm{Ordinal},\\ Iff( \\partialOrder.lt c (a \\nabla b),\\ Exists a' < a, \\ Exists b' < b,\\ partialOrder.le (c. nadd (a'.nmul b')) ((a'.nmul b).nadd (a.nmul b')))$$$$
Lean4
theorem nmul_comm (a b) : a ⨳ b = b ⨳ a := by
rw [nmul, nmul]
congr; ext x; constructor <;> intro H c hc d hd
· rw [nadd_comm, ← nmul_comm, ← nmul_comm a, ← nmul_comm d]
exact H _ hd _ hc
· rw [nadd_comm, nmul_comm, nmul_comm c, nmul_comm c]
exact H _ hd _ hc
termination_by (a, b)
