English
Let α be a commutative monoid with zero which is a WfDvdMonoid. Then the divisibility relation restricted to nonunits (x ∣ y and y is not a unit) is well-founded; equivalently, there is no infinite sequence x0, x1, x2, … with xi ∣ xi+1 and xi+1 not a unit for all i.
Русский
Пусть α — коммутативный моноид с нулём, удовлетворяющий условию хорошей основанности делимости. Тогда отношение делимости между элементами, не являющимися единицами, является хорошо основанным: не существует бесконечной последовательности x0 | x1 | x2 | …, где каждый xi не является единицей.
LaTeX
$$$\mathrm{WellFounded}\big(\mathrm{DvdNotUnit}(\alpha)\big) \quad\text{under assumption } [\text{CommMonoidWithZero }\alpha] \, [\text{WfDvdMonoid }\alpha].$$$
Lean4
theorem wellFounded_dvdNotUnit {α : Type*} [CommMonoidWithZero α] [h : WfDvdMonoid α] :
WellFounded (DvdNotUnit (α := α)) :=
h.wf
