English
Let o be NF and split o = (oadd(e, n, a), m). Then the sum repr(a) + m is strictly less than ω^{repr(e)}.
Русский
Пусть o — NF и split o = (oadd(e, n, a), m). Тогда repr(a) + m строго меньше чем ω^{repr(e)}.
LaTeX
$$$\\forall o\,e\,n\,a\,m\\,[NF\\ o]\\;\\big( split\\ o = (oadd\\ e\\ n\\ a, m) \\big) \\Rightarrow \\operatorname{repr} a + m < \\omega^{\\operatorname{repr} e}$$$
Lean4
theorem split_add_lt {o e n a m} [NF o] (h : split o = (oadd e n a, m)) : repr a + m < ω ^ repr e :=
by
obtain ⟨h₁, h₂⟩ := nf_repr_split h
obtain ⟨e0, d⟩ := h₁.of_dvd_omega0 (split_dvd h)
apply principal_add_omega0_opow _ h₁.snd'.repr_lt (lt_of_lt_of_le (nat_lt_omega0 _) _)
simpa using opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0)
