proposition: Lemma tab_eqP p q : is_tableau p -> is_tableau q -> reflect (forall i, nth [::] p i = nth [::] q i) (p == q).
proof: Proof. Proof using. move=> Hp Hq. apply (iffP idP) => [/eqP -> // | H]. have Hnth t i : nth 0 (shape t) i = size (nth [::] t i). case: (ltnP i (size t)) => Hi. - by rewrite /shape (nth_map [::] _ _ Hi). - by rewrite !nth_default // size_map. have Hsz : size p = size q. rewrite -!(size_map size); congr (size _). apply/eqP/(part_eqP (is_part_sht Hp) (is_part_sht Hq)) => i. by rewrite !Hnth H. by apply/eqP; apply (eq_from_nth (x0 := [::]) Hsz) => i _. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted