proposition: Lemma mem_RSclass w : w \in (RSclass (RS w)).
proof: Proof. Proof using. apply negbNE; apply/count_memPn. by rewrite RSclass_countE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab