proposition: Lemma eval_PolyComb e sq sc : eval_poly e (PolyComb sq sc) = poly_comb (map (eval_poly e) sq) sc.
proof: Proof. rewrite /PolyComb /poly_comb size_map -bigop.unlock -val_enum_ord/= big_map. rewrite (@big_morph _ _ _ 1%R *%R _ _ (eval_MulPoly _))/= ?mul0r ?add0r//. by rewrite big_enum; under eq_bigr do rewrite eval_ExpPoly/= -(nth_map _ 0)//. 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)