proposition: Lemma sumn_shape_stdtabnE (Q : stdtabn) : (sumn (shape Q)) = n.
proof: Proof. Proof using. by case: Q => q; rewrite /is_stdtab_of_n /= => /andP[H /= /eqP]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau