fact: Definition is_RStabpair (pair : TabPair) := let: (P, Q) := pair in [&& is_tableau P, is_stdtab Q & (shape P == shape Q)].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab