proposition: Fact finite_stdtabsh : Finite.axiom stdtabsh_enum.
proof: Proof. Proof using. case=> /= t Ht; rewrite -(count_map _ (pred1 t)) (pmap_filter (@insubK _ _ _)). rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first. by rewrite isSome_insub; case: eqP=> // ->. move: Ht => /andP[Htab /eqP]. rewrite -(shape_yam_of_stdtab Htab) => Hsht. rewrite /enum_stdtabsh count_map. rewrite (eq_in_count (a2 := pred1 (yam_of_stdtab t))); first last. move=> y /(allP (enum_yamevalP (intpartP sh))). rewrite /is_yam_of_eval => /andP[Hyam /eqP Hevy] /=. apply/idP/idP => /eqP H; apply/eqP. + by rewrite -H stdtab_of_yamK. + by rewrite H yam_of_stdtabK. apply: (enum_yameval_countE (intpartP sh)). by rewrite /is_yam_of_eval yam_of_stdtabP //= Hsht. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau