proposition: Lemma alt_syme (m : 'X_{1..n}) k : 'a_(m + rho) * 'e_k = \sum_(h : {set 'I_n} | #|h| == k) 'a_(m + mesym1 h + rho).
proof: Proof. Proof using . rewrite /alternpol exchange_big /=. rewrite mulr_suml; apply eq_bigr => s _. rewrite -(issymP _ (mesym_sym n R k) s) mesymE. rewrite (raddf_sum (@msym _ _ _)) /=. rewrite mulr_sumr; apply eq_bigr => h _. rewrite -scalerAl -msymM -mpolyXD. by rewrite -!addmA [(mesym1 h + rho)%MM]addmC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn