proposition: Lemma mesym_SchurE d : mesym n R d = Schur n0 R (colpartn d).
proof: Proof. Proof using. rewrite /= mesym_tupleE /tmono Schur_tabsh_readingE. rewrite (eq_bigl _ _ (@tabwordshape_col d)). under [LHS]eq_bigr => i do have /permPl/(perm_big _) <- /= := perm_rev i. rewrite (eq_bigl (fun i => sorted >%O (rev_tuple i))); first last. move=> [t /= _]; rewrite rev_sorted sorted_map. exact: eq_sorted. by apply/esym/reindex/onW_bij/inv_bij => x; apply val_inj; rewrite /= revK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau