rw [Set.mem_Ioi] at ha hb
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : a ∈ Set.Ioi c
b : R
hb : b ∈ Set.Ioi c
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹