proposition: Lemma is_tableauP t : reflect [/\ forall i, i < size t -> (nth [::] t i) != [::], forall i, is_row (nth [::] t i) & forall i j, i < j -> dominate (nth [::] t j) (nth [::] t i)] (is_tableau t).
proof: Proof. Proof using. apply (iffP idP). - elim: t => [_ | t0 t IHt] /=. split=> i //=; first by rewrite nth_default. by move=> j; rewrite !nth_default. move=> /and4P[Ht0 Hrow0 Hdom0 {}/IHt [Hnnil Hrow Hdom]]. split; try by case. case=> [| i] [| j] //=. + case: j => [|j] _; first by rewrite nth0. apply: (dominate_trans _ _ _ _ Hdom0). by rewrite -nth0; apply: Hdom. + by rewrite ltnS; apply: Hdom. - elim: t => [| t0 t IHt] //= [Hnnil Hrow Hdom]. apply/and4P; split. + exact: (Hnnil 0). + exact: (Hrow 0). + move: Hdom; case t => [| t1 tt] //= H. rewrite -/(nth [::] (t0 :: t1 :: tt) 0) -/(nth [::] (t0 :: t1 :: tt) 1). exact: H. + apply IHt; split => [i H | i | i j H]. * exact: (Hnnil i.+1). * exact: (Hrow i.+1). * exact: (Hdom i.+1 j.+1). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted