convert inv_sub_antitoneOn_gt (R:=R) 0
R : Type u_1
inst✝ : LinearOrderedField R
⊢ AntitoneOn (fun x => x⁻¹) (Set.Ioi 0)
case h.e'_5.h.h.e'_3
R : Type u_1
inst✝ : LinearOrderedField R
x✝ : R
⊢ x✝ = x✝ - 0