proposition: Fact stdtabn_of_sh_subproof (t : stdtabsh sh) : is_stdtab_of_n n t.
proof: Proof. move: t => [t /= /andP[->/= /eqP eqsh]]. by rewrite /size_tab eqsh sumn_intpartn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau