proposition: Lemma eq_from_shape_get_tab (t u : seq (seq T)) : shape t = shape u -> get_tab t =1 get_tab u -> t = u.
proof: Proof. Proof using. move=> Hsh Hget; apply (eq_from_nth (x0 := [::])). by rewrite -!(size_map size) -!/(shape _) Hsh. move=> r _; apply: (eq_from_nth (x0 := inh)). by rewrite -!nth_shape Hsh. by move=> c _; rewrite -!/(get_tab _ (_, _)) Hget. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau