English
If nextCoeff ≠ 0, then P.coeffList equals the leadingCoeff cons the coeffList of eraseLead, after adjusting by natDegree arithmetic.
Русский
Если следующий коэффициент не равен 0, то P.coeffList начинается с ведущего коэффициента и затем идёт coeffList от eraseLead с корректировкой.
LaTeX
$$$ P.nextCoeff \\neq 0 \\Rightarrow P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList $$$
Lean4
theorem leadingCoeff_cons_eraseLead (h : P.nextCoeff ≠ 0) : P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList :=
by
have h₂ := ne_zero_of_natDegree_gt (natDegree_pos_of_nextCoeff_ne_zero h)
have h₃ := mt nextCoeff_eq_zero_of_eraseLead_eq_zero h
simpa [natDegree_eraseLead_add_one h, coeffList, withBotSucc_degree_eq_natDegree_add_one h₂,
withBotSucc_degree_eq_natDegree_add_one h₃, List.range_succ] using (Polynomial.eraseLead_coeff_of_ne · ·.ne)
