English
Let b be an ordinal and h : NF (ONote.oadd e n a). If ω^b divides repr (ONote.oadd e n a), then b ≤ repr e and ω^b divides repr a.
Русский
Пусть b — акр ord, и h: NF (ONote.oadd e n a). Если ω^b делит repr (ONote.oadd e n a), то b ≤ repr e и ω^b делит repr a.
LaTeX
$$$\forall b:\, Ordinal,\; \forall e\, n\, a,\; (e.oadd n a).NF \rightarrow (\omega^b) \mid (e.oadd n a).repr \Rightarrow b \leq repr(e) \wedge (\omega^b) \mid repr(a)$$$
Lean4
theorem of_dvd_omega0_opow {b e n a} (h : NF (ONote.oadd e n a)) (d : ω ^ b ∣ repr (ONote.oadd e n a)) :
b ≤ repr e ∧ ω ^ b ∣ repr a :=
by
have := mt repr_inj.1 (fun h => by injection h : ONote.oadd e n a ≠ 0)
have L := le_of_not_gt fun l => not_le_of_gt (h.below_of_lt l).repr_lt (le_of_dvd this d)
simp only [repr] at d
exact ⟨L, (dvd_add_iff <| (opow_dvd_opow _ L).mul_right _).1 d⟩
