exact inv_sub_antitoneOn_gt c |>.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha
case pos
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
hab : a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
no goals