proposition: Lemma tabsh_reading_RSE sh : tabsh_reading sh =1 tabsh_reading_RS sh.
proof: Proof. Proof using . move=> w. apply/idP/idP. - by move /tabsh_readingP/tabsh_reading_RSP. - by move /tabsh_reading_RSP/tabsh_readingP. 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