proposition: Lemma eval_amulXnT (a : tF) (n : nat) (e : seq F) : eval_poly e (amulXnT a n) = (eval e a)%:P * 'X^n.
proof: Proof. elim: n=> [|n] /=; first by rewrite expr0 mulr1 mul0r add0r. by move->; rewrite addr0 -mulrA -exprSr. 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)