∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {P : Polynomial R},
  P ≠ 0 →
    P.signVariations =
      P.eraseLead.signVariations +
        if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0