proposition: Lemma msym_map_mpoly s (p : {mpoly R[n]}) : msym s (map_mpoly mor p) = map_mpoly mor (msym s p).
proof: Proof. Proof using. rewrite (mpolyE p). rewrite [map_mpoly _ _]raddf_sum [msym s _]raddf_sum. rewrite [msym s _]raddf_sum [map_mpoly _ _]raddf_sum. apply eq_bigr => i _ /=; apply/mpolyP => m. by rewrite mcoeff_map_mpoly /= !mcoeff_sym mcoeff_map_mpoly. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition