proposition: Lemma RSclass_countE w : count_mem w (RSclass (RS w)) = 1.
proof: Proof. Proof using. rewrite count_map. rewrite (eq_in_count (a2 := pred1 ((RSmap w).2))); first last. move=> y /= /(allP (enum_yamevalP (is_part_sht (is_tableau_RS _)))). rewrite /is_yam_of_eval => /andP[Hyam /eqP Hsh]. apply/idP/idP => /eqP H. - by rewrite -{}H RSmapinv2K //= (is_tableau_RS _) Hyam Hsh /=. - by rewrite {}H -RSmapE -surjective_pairing RSmapK. apply: (enum_yameval_countE (is_part_sht (is_tableau_RS _))). rewrite /is_yam_of_eval -shape_RSmap_eq RSmapE eq_refl andbT. exact: is_yam_RSmap2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab