proposition: Lemma eval_natmulpT (p : polyF) (n : nat) (e : seq F) : eval_poly e (natmulpT n p) = (eval_poly e p) *+ n.
proof: Proof. elim: p; rewrite //= ?mul0rn // => c p ->. rewrite mulrnDl mulr_natl polyCMn; congr (_ + _). by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC. 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)