rewrite [this]
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded fun a b => (fun x x_1 => x < x_1) ↑a ↑b
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded (Measure fun x => Int.natAbs (↑x - a))