apply Iff.intro
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 ↔ ↑x - a < ↑y - a
case h.h.a.mp
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y → ↑x - a < ↑y - a

case h.h.a.mpr
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x - a < ↑y - a → ↑x < ↑y