English
If p and q are monic, then nextCoeff(p q) = nextCoeff(p) + nextCoeff(q).
Русский
Если p и q моноические, то nextCoeff(p q) = nextCoeff(p) + nextCoeff(q).
LaTeX
$$$Monic(p) \land Monic(q) \Rightarrow \text{nextCoeff}(p q) = \text{nextCoeff}(p) + \text{nextCoeff}(q)$$$
Lean4
theorem nextCoeff_mul (hp : Monic p) (hq : Monic q) : nextCoeff (p * q) = nextCoeff p + nextCoeff q :=
by
nontriviality
simp only [← coeff_one_reverse]
rw [reverse_mul] <;> simp [hp.leadingCoeff, hq.leadingCoeff, mul_coeff_one, add_comm]