proposition: Lemma RSpairyamQ : is_RSpair (yamtab (shape Q), yam_of_stdtab Q).
proof: Proof. Proof using . rewrite /= yamtabP /=; last by apply: is_part_sht; exact: stdtabP. by rewrite yam_of_stdtabP //= shape_yam_of_stdtab // shape_yamtab. 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