∀ {R : Type u_1} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : NoZeroDivisors R]
  [inst_3 : OreLocalization.OreSet (nonZeroDivisors R)] (x : ℚ≥0) (x_1 : OreLocalization (nonZeroDivisors R) R),
  ↑x * x_1 = ↑x * x_1