proposition: Lemma is_tableau_getP t : reflect [/\ is_part (shape t), (forall (r c : nat), in_shape (shape t) (r, c.+1) -> (get_tab t (r, c) <= get_tab t (r, c.+1))%O) & (forall (r c : nat), in_shape (shape t) (r.+1, c) -> (get_tab t (r, c) < get_tab t (r.+1, c))%O)] (is_tableau t).
proof: Proof. Proof using. rewrite is_tableau_sorted_dominate. apply/(iffP idP) => [|[Hpart]]. - move=> /and3P[Hpart /allP Hrow /(sorted_strictP _ dominate_rev_trans)] Hdom. split; rewrite /get_tab => // r c Hin. + have/Hrow/is_row1P : (nth [::] t r) \in t. by apply/mem_nth/in_shape_tab_size/Hin. by apply; exact: in_shape_tab. + have/(Hdom [::])/dominateP[_] : r < r.+1 < size t. by rewrite ltnSn (in_shape_tab_size Hin). by apply; exact: in_shape_tab. - rewrite /get_tab Hpart => Hrow Hcol /=; apply/andP; split. + apply/allP => /= c Hrin. have Hr := nth_index [::] Hrin. move: Hrin Hr; rewrite -index_mem; move: (index c t) => r Hr Hc; subst c. apply/is_row1P => i Hi; apply Hrow. by rewrite /in_shape (nth_map [::]). + apply/(sorted_strictP [::] dominate_rev_trans). rewrite (incr_equiv _ dominate_rev_trans) => r Hr. apply/dominateP; split. * rewrite -!(nth_map _ 0) -/shape //; last by move: Hr; apply ltnW. by move/is_partP: Hpart => [_]. * move=> i Hi; apply Hcol. by rewrite /in_shape (nth_map [::]). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted