∀ {R : Type u_1} [inst : CommRing R] [inst_1 : ValuativeRel R] (r : R) (s : ↥(ValuativeRel.posSubmonoid R)),
  (ValuativeRel.valuation R) r / (ValuativeRel.valuation R) ↑s = ValuativeRel.ValueGroupWithZero.mk r s