gcongr
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)⁻¹
case ha
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ 0 < a - c