proposition: Lemma eval_NatMulPoly p n e : eval_poly e (n +** p)%qfT = (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: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)