ext x y
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
⊢ (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Measure (fun x => Int.natAbs (↑x - a)) x y