proposition: Lemma eval_ScalPoly e t p : eval_poly e (ScalPoly t p) = (eval e t) *: (eval_poly e p).
proof: Proof. elim: p=> [|a p ihp] /=; first by rewrite scaler0. by rewrite ihp scalerDr scalerAl -!mul_polyC rmorphM. 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)