proposition: Lemma is_tableau_RSmap1 w : is_tableau (RSmap w).1.
proof: Proof. Proof using. rewrite /RSmap RSmapE; apply: is_tableau_RS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab