∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {P : Polynomial R} (cs : List R),
  (SignType.sign P.leadingCoeff ::
          List.destutter' (fun x1 x2 => ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x => !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 => ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x => !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
        1 +
      1