proposition: Lemma is_stdtab_RStabmap2 (w : seq T) : is_stdtab (RStabmap w).2.
proof: Proof. Proof using. have:= RStabmap_spec w; rewrite /is_RStabpair. by case: (RStabmap w) => [P Q] /and3P[] /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab