proposition: Lemma RStabinvK : cancel RStabinv RStab.
proof: Proof. Proof using. rewrite /RStab /RStabinv /RStabmap. move=> [[P Q] H] /=; apply: pqpair_inj => /=. move: H; rewrite /is_RStabpair => /and3P[Htab Hstdtab Hshape] //=. rewrite RSmapinv2K. + by rewrite (yam_of_stdtabK Hstdtab). + by rewrite /is_RSpair Htab yam_of_stdtabP //= shape_yam_of_stdtab. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab