proposition: Lemma RSperm n (p : 'S_n) : is_stdtab (RS (wordperm p)).
proof: Proof. rewrite /is_stdtab; apply/andP; split; first exact: is_tableau_RS. apply: (perm_std (wordperm_std p)). by rewrite perm_sym; apply: (perm_RS (wordperm p)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab