refine antitoneOn_iff_forall_lt.mpr ?_
R : Type u_1
inst✝ : LinearOrderedField R
c : R
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Ioi c)
R : Type u_1
inst✝ : LinearOrderedField R
c : R
⊢ ∀ ⦃a : R⦄, a ∈ Set.Ioi c → ∀ ⦃b : R⦄, b ∈ Set.Ioi c → a < b → (b - c)⁻¹ ≤ (a - c)⁻¹