proposition: Lemma conj_stdtabnP n (t : stdtabn n): is_stdtab_of_n n (conj_tab t).
proof: Proof. case: t => t /= /andP[Ht /eqP Hsh]. rewrite (is_stdtab_conj Ht) /=. by rewrite /size_tab shape_conj_tab sumn_conj_part -/(size_tab _) Hsh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau