∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommRing R] {b : MvPolynomial σ R}
  (hb : IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R),
  m.reduce hb f = f - (MvPolynomial.monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f) * b