proposition: Lemma is_skew_tableauP inner t : reflect [/\ size inner <= size t, forall i, i < size t -> nth 0 inner i + size (nth [::] t i) != 0, forall i, is_row (nth [::] t i) & forall i, skew_dominate ((nth 0 inner i) - (nth 0 inner i.+1)) (nth [::] t i.+1) (nth [::] t i)] (is_skew_tableau inner t).
proof: Proof. Proof using. apply (iffP idP). - elim: t inner => [| t0 t IHt] /= inner. by move=> /eqP ->; split=> // i; rewrite !nth_default. case: inner => [| inn0 inn] /and4P[Ht0 Hrow0 Hdom0 /= /IHt[Hsz Hnnil Hrow Hdom]]. + split. * by []. * case=> [_| i] /=; first exact: Ht0. by rewrite ltnS => /Hnnil; rewrite nth_default. * by case. * case=> [| i] /=; first by move: Hdom0; rewrite /= subn0. by move/(_ i) : Hdom => /=; rewrite nth_default // subn0. + split. * exact: Hsz. * case=> [_| i] /=; last by rewrite ltnS; exact: Hnnil. by move: Ht0. * by case. * case=> [| i] /=; first exact: Hdom0. by move/(_ i) : Hdom => /=; case inn; rewrite // nth_default. - elim: t inner => [| t0 t IHt] inner //= [Hsz Hnnil Hrow Hdom]. by move: Hsz; rewrite leqn0 => /nilP ->. apply/and4P; split. + by have /Hnnil := ltn0Sn (size t); case inner. + by rewrite -/(nth [::] (t0 :: t) 0); exact: Hrow. + by move: Hdom; case t => //= t1 tt /(_ 0); case inner. + apply IHt; split => [| i Hi | i | i]. * by move: Hsz; case inner. * move: Hi; rewrite -ltnS => /Hnnil. by case inner; rewrite //= [nth 0 [::] i]nth_default. * exact: (Hrow i.+1). * move/(_ i.+1) : Hdom. by case inner => [|_ [| inn]] //=; rewrite [nth 0 [::] i]nth_default. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab