proposition: Lemma msymE p (s : 'S_n) k : msize p <= k -> msym s p = \sum_(m : 'X_{1..n < k}) (p@_m *: 'X_[m#(s^-1)%g]).
proof: Proof. move=> lt_pk; rewrite /msym (mmapE k) //=; apply/eq_bigr. move=> m' _; rewrite mul_mpolyC; congr (_ *: _). rewrite /mmap1 mprodXnE [X in _=X]mpolyXE_id mprodXnE. rewrite [X in _='X_[X]](reindex (fun i : 'I_n => s i)) /=. congr 'X_[_]; apply/eq_bigr=> i _; congr (_ *+ _)%MM. by rewrite mnmE /= permK. by exists (s^-1)%g=> i _; rewrite (permK, permKV). 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