proposition: Lemma is_part_shape_deg (Q : stdtabn) : is_part_of_n n (shape Q).
proof: Proof. Proof using. rewrite /=; apply/andP; split. - by rewrite -/(size_tab _) size_tab_stdtabn. - apply: is_part_sht; apply stdtabP; apply: stdtabnP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau