proposition: Fact finite_stdtabn : Finite.axiom stdtabn_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 -(size_yam_of_stdtab Htab) => Hszt. rewrite /enum_stdtabn map_comp enum_unionE count_map. rewrite (eq_in_count (a2 := pred1 (yam_of_stdtab t))); first last. move=> y /(allP (all_unionP _ yamn_PredEq)) /=. rewrite /is_yam_of_size => /andP[Hyam /eqP Hszy] /=. apply/idP/idP => /eqP H; apply/eqP. + by rewrite -H stdtab_of_yamK. + by rewrite H yam_of_stdtabK. apply: (count_unionP _ yamn_PredEq). - exact: yamn_partition_evalseq. - by rewrite /is_yam_of_size yam_of_stdtabP //= Hszt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau