proposition: Lemma eval_sumpT (p q : polyF) (e : seq F) : eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e q).
proof: Proof. elim: p q => [|a p Hp] q /=; first by rewrite add0r. case: q => [|b q] /=; first by rewrite addr0. rewrite Hp mulrDl -!addrA; congr (_ + _); rewrite polyCD addrC -addrA. by congr (_ + _); rewrite addrC. 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)