proposition: Theorem RStabmap_spec w : is_RStabpair (RStabmap w).
proof: Proof. Proof using. have:= RSmap_spec w; rewrite /is_RStabpair /is_RSpair /RStabmap. case H : (RSmap w) => [P Q] /and3P[-> /stdtab_of_yamP-> /eqP->] /=. by rewrite shape_stdtab_of_yam. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab