proposition: Lemma mcoeff_map_mpoly m p : p^f@_m = f p@_m.
proof: Proof. pose_big_enough i; first rewrite (map_mpolyE i) //. by rewrite (mcoeff_mpoly (fun m => (f p@_m))). by close. 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