proposition: Lemma RSclassE tab w : is_tableau tab -> w \in RSclass tab = (RS w == tab).
proof: Proof. Proof using. move=> Htab /=; apply/idP/idP. - by move: Htab=> /RSclassP/allP/[apply]. - move/eqP => Hw. apply/mapP; exists (RSmap w).2. + apply/count_memPn. rewrite (enum_yameval_countE (is_part_sht Htab)) //=. rewrite /is_yam_of_eval is_yam_RSmap2 /=. by rewrite -shape_RSmap_eq RSmapE Hw. + by rewrite -Hw -RSmapE -surjective_pairing RSmapK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab