proposition: Lemma card_stdtabsh_conj_part (sh : intpart) : #|{:stdtabsh (conj_part sh)}| = #|{:stdtabsh sh}|.
proof: Proof. by symmetry; apply: (bij_eq_card (conj_stdtabsh_bij sh)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau