∀ {R : Type u_2} [inst : Ring R] [NoZeroDivisors R] [Nontrivial R] {x : R} {P : Polynomial R},
  x ≠ 0 →
    P.nextCoeff = 0 →
      ((Polynomial.X - Polynomial.C x) * P).eraseLead.eraseLead = (Polynomial.X - Polynomial.C x) * P.eraseLead