English
The greater-than relation on Nat.Upto is well-founded if there exists a value satisfying p.
Русский
Отношение > на Nat.Upto хорошо упорядочено (well-founded) если существует значение, удовлетворяющее p.
LaTeX
$$$$ \\exists x, p(x) \\Rightarrow \\mathrm{WellFounded}(\\mathrm{Nat.Upto.GT}(p)). $$$$
Lean4
/-- The "greater than" relation on `Upto p` is well founded if (and only if) there exists a value
satisfying `p`. -/
protected theorem wf : (∃ x, p x) → WellFounded (Upto.GT p)
| ⟨x, h⟩ =>
by
suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val
by
rw [this]
exact (measure _).wf
ext ⟨a, ha⟩ ⟨b, _⟩
dsimp [InvImage, Upto.GT]
rw [tsub_lt_tsub_iff_left_of_le (le_of_not_gt fun h' => ha _ h' h)]
