proposition: Lemma eval_opppT (p : polyF) (e : seq F) : eval_poly e (opppT p) = - eval_poly e p.
proof: Proof. by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyCN mul1r. 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)