proposition: Lemma get_conj_tab t : is_part (shape t) -> forall i j, get_tab (conj_tab t) (i, j) = get_tab t (j, i).
proof: Proof. Proof using. move=> Ht i j. case: (boolP (in_shape (shape t) (j, i))) => Hin; have:= Hin; rewrite (in_conj_part Ht) => Hconj. - rewrite {1}/get_tab /conj_tab nth_mkseq; last exact: (in_shape_size Hconj). rewrite -shape_conj_tab. by rewrite nth_mkseq; last by rewrite shape_conj_tab; apply: Hconj. - rewrite /get_tab. rewrite [RHS]nth_default; last by rewrite leqNgt -nth_shape. apply nth_default. by rewrite leqNgt -nth_shape shape_conj_tab. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau