∀ {R : Type u_1} [inst : CommRing R] [NoZeroDivisors R] [inst_2 : NormalizationMonoid R] {a b : Polynomial R},
  a ≠ 0 →
    b ≠ 0 →
      ↑{ val := Polynomial.C ↑(normUnit (a * b).leadingCoeff), inv := Polynomial.C ↑(normUnit (a * b).leadingCoeff)⁻¹,
            val_inv := ⋯, inv_val := ⋯ } =
        ↑({ val := Polynomial.C ↑(normUnit a.leadingCoeff), inv := Polynomial.C ↑(normUnit a.leadingCoeff)⁻¹,
              val_inv := ⋯, inv_val := ⋯ } *
            { val := Polynomial.C ↑(normUnit b.leadingCoeff), inv := Polynomial.C ↑(normUnit b.leadingCoeff)⁻¹,
              val_inv := ⋯, inv_val := ⋯ })