proposition: Theorem perm_RS w : perm_eq w (to_word (RS w)).
proof: Proof. Proof using. by apply/seq.permP => l; exact: count_RS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab