proposition: Lemma syme_to_symm k : 'e_k = 'm[colpartn k] :> SP.
proof: Proof. case: (leqP k n) => [|ltnk]; first last. by rewrite symm_oversize ?size_colpartn ?syme_geqnE. rewrite -{1}(size_colpartn k) => leszn. rewrite (homog_symmE (syme_homog n R k)). rewrite (bigD1 (colpartn k)) //= mcoeff_mesym /mechar. rewrite mdeg_mpart // sumn_intpartn eqxx /=. rewrite [[forall i, _]](_ : _ = true) ?scale1r; first last. apply/forallP => /= i; rewrite /mpart leszn mnmE colpartnE nth_nseq. by case: ltnP. rewrite big1 ?addr0 // => P HP. rewrite mcoeff_mesym /mechar. rewrite [[forall i, _]](_ : _ = false) ?andbF ?scale0r //. move: leszn; rewrite (size_colpartn k) => lekn. apply/negbTE; apply/contra: HP => /forallP /= HP. rewrite /mpart in HP; apply/eqP/(colpartnP (x0 := 1)). case: n lekn HP => [|n0 Hk /(_ ord0)]. by rewrite leqn0 => /eqP Hk _; subst k; rewrite intpartn0 rowpartn0E. have -> := leq_trans (size_part (intpartP P)); last by rewrite sumn_intpartn. by rewrite mnmE /=; case: P => [[|]]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv