∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {η : R} {P : Polynomial R},
  ((Polynomial.X - Polynomial.C η) * P).natDegree = P.natDegree + 1 →
    ∀ (d : ℕ),
      P.natDegree = d + 1 →
        0 < η * P.coeff (d + 1) →
          SignType.sign P.nextCoeff = -1 → SignType.sign ((Polynomial.X - Polynomial.C η) * P).nextCoeff = -1