proposition: Lemma tabword_of_tuple_freeSchur (Q : stdtabn d) : [set tabword_of_tuple x | x in freeSchur Q] = tabwordshape (shape_deg Q).
proof: Proof. Proof using . rewrite /freeSchur /tabwordshape /tabword_of_tuple. apply/setP/subset_eqP/andP; split; apply/subsetP => w; rewrite !inE tabsh_reading_RSE /tabsh_reading_RS. - move/imsetP => [t]; rewrite inE => /eqP HQ /(congr1 val) /= ->. rewrite (RS_tabE (is_tableau_RS t)) eq_refl /= {w}. by rewrite -HQ -!RStabmapE shape_RStabmapE. - move/andP => [/eqP Hw /eqP Hsh]; apply/imsetP. have Hpair : is_RStabpair (RS w, val Q). by rewrite /is_RStabpair is_tableau_RS stdtabnP Hsh eq_refl. have Hpr : is_RSpair (RS w, yam_of_stdtab Q). have:= Hpair; rewrite /is_RStabpair /= => /andP[-> /=]. move=> /andP[/yam_of_stdtabP -> /= /eqP ->]. by rewrite shape_yam_of_stdtab. pose imw := (RStabinv (RSTabPair Hpair)). have Hsz : size (imw) == d. rewrite /imw /RStabinv /= -size_RS -RSmapE. rewrite (RSmapinv2K Hpr) /=. by rewrite size_RS size_tuple. exists (Tuple Hsz). + rewrite inE /= /imw. by have/(congr1 val) := RStabinvK (RSTabPair Hpair) => /= ->. + apply: val_inj => /=. rewrite /imw /RStabinv /= -Hw /=; congr (to_word _). by rewrite Hw -[RS (RSmapinv _ _)]RSmapE RSmapinv2K. 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