proposition: Lemma conj_stdtabshP (sh : intpart) (t : stdtabsh sh) : is_stdtab_of_shape (conj_part sh) (conj_tab t).
proof: Proof. case: t => t /= /andP[Ht /eqP Hsh]. rewrite (is_stdtab_conj Ht) /=. by rewrite shape_conj_tab Hsh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau