∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {P : Polynomial R} (c : R) (cs : List R),
  P.eraseLead.coeffList = c :: cs →
    SignType.sign c = 0 → ¬P.eraseLead = 0 → (∃ ls, P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls) → False