proposition: Lemma eval_Pcq e sq i : eval_poly e (Pcq sq i) = pcq (map (eval_poly e) sq) i.
proof: Proof. rewrite /Pcq /pcq size_map; move: (sg_tab _)=> s. have [ge_is|lt_is] := leqP (size s) i. by rewrite !nth_default ?size_map // /=. rewrite -(nth_map _ 0) ?size_map //; congr _`_i; rewrite -map_comp. by apply: eq_map=> x /=; rewrite eval_PolyComb. 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)