proposition: Lemma eval_mulpT (p q : polyF) (e : seq F) : eval_poly e (mulpT p q) = (eval_poly e p) * (eval_poly e q).
proof: Proof. elim: p q=> [|a p Hp] q /=; first by rewrite mul0r. rewrite eval_sumpT /= Hp addr0 mulrDl addrC mulrAC; congr (_ + _). by elim: q=> [|b q Hq] /=; rewrite ?mulr0 // Hq polyCM mulrDr mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)