∀ {R : Type u_1} [inst : CommRing R] (f₁ f₂ g : Polynomial R) (n : ℕ),
  g.natDegree ≤ n →
    (f₁ * f₂).resultant g (f₁.natDegree + f₂.natDegree) n =
      f₁.resultant g f₁.natDegree n * f₂.resultant g f₂.natDegree n