proposition: Lemma enum_stdtabshE : map val (enum {:stdtabsh}) = enum_stdtabsh sh.
proof: Proof. rewrite enumT unlock /= /stdtabsh_enum /enum_stdtabsh. elim: (enum_yameval sh) (enum_yamevalP (intpartP sh)) => //= y ly IHly. move=> /andP[/andP[Hyam Heval] {}/IHly Hrec]. by rewrite insubT /= stdtab_of_yamP //= ?shape_stdtab_of_yam // Hrec. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau