proposition: Lemma conj_tab_shapeK t : is_part (shape t) -> conj_tab (conj_tab t) = t.
proof: Proof. Proof using. move=> Hpart; apply eq_from_shape_get_tab. - by rewrite !shape_conj_tab conj_partK. - move=> [r c]; rewrite ?get_conj_tab //. by rewrite shape_conj_tab; apply: is_part_conj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau