proposition: Lemma SchurE d (Q : stdtabn d) : Schur (shape_deg Q) = polylang R (tabwordshape (shape_deg Q)).
proof: Proof. Proof using . rewrite Schur_tabsh_readingE /polylang /commword; apply eq_bigl => i /=. by rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly