proposition: Lemma size_conj_tab t : size (conj_tab t) = size (conj_part (shape t)).
proof: Proof. Proof using. by rewrite /conj_tab size_mkseq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau