core / init.wf
A relation r : α → α → Prop is well-founded when ∀ x, (∀ y, r y x → P y → P x) → P x for all predicates P.
Once you know that a relation is well_founded, you can use it to define fixpoint functions on α.
r : α → α → Prop
∀ x, (∀ y, r y x → P y → P x) → P x
Well-founded fixpoint satisfies fixpoint equation
Empty relation is well-founded
less-than is well-founded