∀ {R : Type u_1} [inst : MonoidWithZero R] [inst_1 : Nontrivial R] [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)]
  [inst_3 : NoZeroDivisors R] (x : OreLocalization (nonZeroDivisors R) R), x ≠ 0 → x * x⁻¹ = 1