proposition: Lemma comp_mpoly_meval : (p \mPo lq).@[v] = p.@[fun i => (tnth lq i).@[v]].
proof: Proof. rewrite comp_mpolyEX [X in _ = X.@[_]](mpolyE p) !raddf_sum /=. apply/eq_bigr => m _; rewrite !mevalZ; congr *%R. rewrite comp_mpolyX rmorph_prod /= mevalX. by apply/eq_bigr=> i _; rewrite rmorphXn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg