proposition: Lemma RStabmapE (w : seq T) : (RStabmap w).1 = RS w.
proof: Proof. Proof using. by rewrite /RStabmap -RSmapE; case RSmap. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab