∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {β : Type u_3}
  [inst_3 : DivisionRing β] (abv : β → α) [IsAbsoluteValue abv] {ε K : α},
  0 < ε → 0 < K → ∃ δ > 0, ∀ {a b : β}, K ≤ abv a → K ≤ abv b → abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε