proposition: Lemma join_tab_skew s t : all (allLtn (to_word s)) (to_word t) -> is_tableau s -> is_skew_tableau (shape s) t -> is_tableau (join_tab s t).
proof: Proof. Proof using. rewrite /join_tab. elim: s t => [| s0 s IHs] /= t. move => _ _ Ht; rewrite subn0 /=. rewrite [map _ _](_ : _ = t); last by elim: t {Ht} => //= r t ->. by rewrite -is_skew_tableau0. rewrite to_word_cons => /all_allLtn_cat [Halls Halls0]. move/and4P => [Hnnils0 Hrows0 Hdoms Htabs]. case: t Halls0 Halls => [// | t0 t] Halls0 Halls. move=>/and4P[Hszt0 Hrowt0 Hdomt Htabt]. apply/and4P; rewrite subSS; split. - by move: Hnnils0; apply contra; case s0. - move: Halls0; rewrite to_word_cons all_cat => /andP[_]. move=> {s Hdoms Hszt0 Hdomt IHs Htabs Htabt Halls}. case: s0 Hnnils0 Hrows0 => //= l0 s0 _ Hpath /allP. rewrite cat_path {}Hpath /=. case: t0 Hrowt0 => //= m0 t0 /= Hpath Hall. apply/andP; split; last exact Hpath. have {}/Hall /andP[] : m0 \in m0 :: t0 by rewrite in_cons eq_refl. case/lastP: s0 => [/ltW // | s0 sn] /= _. by rewrite last_rcons /allLtn all_rcons /= => /andP[/ltW]. - move=> {IHs Hrows0 Hrowt0 Hnnils0 Hszt0 Halls}. case: s Hdoms Htabs Hdomt Htabt => [_ _| s1 s] /=. + rewrite subn0. case: t Halls0 => //= t1 t Halls0 /dominateP[Hszt Hdomt] _. apply/dominateP; split. * by move: Hszt; rewrite size_cat size_drop leq_subLR. * move: Halls0; rewrite !to_word_cons. rewrite !all_cat => /andP[/andP[_ Hallt1] Hallt0] i Hi. rewrite nth_cat; case ltnP => His0. * move: Hallt1 => /allP/(_ _ (mem_nth inh Hi)). by rewrite /allLtn => /allP/(_ _ (mem_nth inh His0)) /=. * have /Hdomt : (i - size s0) < size (drop (size s0) t1). by rewrite size_drop ltn_subRL (subnKC His0). by rewrite nth_drop (subnKC His0). + case: t Halls0 => //= t1 t Halls0 /dominateP[Hszs Hdoms] _. move: Halls0; rewrite !to_word_cons. rewrite !all_cat => /andP[/andP[_ Hallt1] Hallt0]. move/dominateP => [Hszt Hdomt] _ {s t}. have {}Hszt : size s1 + size t1 <= size s0 + size t0. by move: Hszt; rewrite size_drop (subnBA _ Hszs) leq_subLR addnC. apply/dominateP; split; first by rewrite !size_cat. rewrite size_cat => i Hi. rewrite !nth_cat. case: (ltnP i (size s1)) => Hi1. by rewrite (leq_trans Hi1 Hszs); apply Hdoms. case: (ltnP i (size s0)) => Hi0. * move: Hallt1 => /allP Hallt1; move: Hi. rewrite -{1}(subnKC Hi1) ltn_add2l => /(mem_nth inh) {}/Hallt1. by rewrite /allLtn => /allP/(_ _ (mem_nth inh Hi0)). * have /Hdomt : i - size s0 < size (drop (size s0 - size s1) t1). rewrite size_drop -(ltn_add2l (size s0)) (subnKC Hi0). rewrite (subnBA _ Hszs) subnKC addnC //=. by apply (leq_trans Hi0); exact: ltnW. by rewrite nth_drop addnC (addnBA _ Hszs) (subnK Hi0). - apply: (IHs _ _ Htabs Htabt). by move: Halls; rewrite to_word_cons all_cat => /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab