Nat.Upto.wf

theorem Nat.Upto.wf : ∀ {p : ℕ → Prop}, (∃ x, p x) → WellFounded (Nat.Upto.GT p)

The theorem `Nat.Upto.wf` states that for any property `p` mapping natural numbers to propositions, if there exists a natural number `x` that satisfies this property `p`, then the "greater than" relation on the set `Upto p` of natural numbers up to `x` is well-founded. In the context of order theory, a relation is well-founded if there are no infinite descending chains, which in this case means there are no infinite sequences of elements of `Nat.Upto p` where each element is greater than the next.

More concisely: If a property `p` mapping natural numbers to propositions has an element with the smallest index, then the "greater than" relation on the set of numbers up to that index in `p` is well-founded.