proposition: Lemma bij_LRsupportP : is_stdtab_of_n (d1 + d2) (RStab (changeUT T1 T2 (RSmapinv2 (yamtab (shape Q), yam_of_stdtab Q)))).2.
proof: Proof. Proof using . rewrite /is_stdtab_of_n /=. apply/andP; split; first exact: is_stdtab_RStabmap2. rewrite /size_tab /= -shape_RStabmapE RStabmapE -/(size_tab _) size_RS size_cat. by rewrite !size_RSmapinv2_yam. 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