proposition: Lemma is_tab_append_nth_size r T n : all (gtn n) (to_word T) -> is_part (incr_nth (shape T) r) -> is_tableau T -> is_tableau (append_nth T n r).
proof: Proof. elim: T r => [// | T0 T IHT] r /=; first by case: r => [// | r] /=; elim: r. rewrite to_word_cons all_cat. move=> /andP[Hall Hall0]. case: r => [/= _ | r] /=. - move=> {IHT Hall} /and4P[Hnnil Hrow Hdom ->]. rewrite (dominate_rcons _ Hdom) {Hdom} !andbT. apply/andP; split; first by case T0. apply: (is_row_rcons Hrow); rewrite {Hrow} leEnat. case/lastP: T0 Hall0 {Hnnil} => [// | T0 T0n]. rewrite all_rcons last_rcons /= andbC => /andP[_]. exact: ltnW. - move => /andP[Hhead Hpart] /and4P[-> -> Hdom Htab] /=. rewrite {}IHT //= andbT {Hall Hpart Htab}. case: r Hhead => [| r]; last by case: T Hdom => [// | T1 T]. case: T Hdom => [_ | T1 T] /=. + case: T0 Hall0 => [// | hT0 T0] /= /andP[Hn _] _. by rewrite /dominate /= andbT. + move/dominateP => [_ Hdom Hsize]. apply/dominateP; split; rewrite size_rcons; first by []. move=> i Hi; rewrite nth_rcons; case: (ltnP i (size T1)) => Hi1. * exact: Hdom. * have -> : i == size T1 by rewrite eqn_leq Hi1 andbT -ltnS. move: Hall0 => /allP Hall0. by have /Hall0 /= := mem_nth inh (leq_trans Hi Hsize). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau