∀ {R : Type u_1} [inst : Semiring R] {P : Polynomial R} (c : R) (cs : List R),
  P.eraseLead.coeffList = c :: cs →
    ∀ (ls : List R), P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls → c = P.eraseLead.leadingCoeff