proposition: Lemma remnP t : is_stdtab t -> t != [::] -> is_tableau (remn t) /\ append_nth (remn t) (size_tab t).-1 (last_big t (size_tab t).-1) = t.
proof: Proof. rewrite /remn; move Hn : (size_tab t) => n. case: n Hn => [| n Hsize Hstdtab _]; first by move=> /tab0 H /andP[/H ->]. have:= Hstdtab => /andP[Htab Hstd]. have Hperm : perm_eq (to_word t) (iota 0 n.+1) by rewrite -Hsize -size_to_word. have:= std_uniq Hstd. have {Hsize Hstdtab Hstd} : allLeq (to_word t) n. have:= Hstd => /perm_allLeqE ->. apply/allP => x. by rewrite mem_iota add0n size_to_word Hsize /= leEnat. have {Hperm} : n \in to_word t. by move: Hperm => /perm_mem ->; rewrite mem_iota /= add0n. elim: t Htab => [// | t0 t' /= IHt] /and4P[]. case: t0 => [| l0 t0] _ //. case/altP: ((last l0 t0) =P n). - case/lastP: t0 {IHt} => [ /= Hl0 _ | t0 tn]. rewrite !dominate_recE; subst l0. case: t' => [//=| t1 t'] /= Hdom /and4P[Hnnil _ _ _] _. rewrite !to_word_cons !allLeq_catE => /andP[/andP[_ Ht1] _] _. exfalso. case: t1 Hnnil Ht1 Hdom => [// | l1 t1] _ /= /andP[Hl1 _]. case: t1 => /=; rewrite ?andbF ?andbT //. by rewrite ltNge Hl1. rewrite rcons_nilF belast_rcons last_rcons => Hl0. subst tn => Hrow Hdom Htab' _ /=. rewrite to_word_cons cat_uniq allLeq_catE => /andP[Ht' _] /and3P[_]. rewrite -all_predC => /allP /= Hall _. have {}/Hall Hn : n \in l0 :: rcons t0 n. by rewrite inE mem_rcons inE eq_refl orbT. move: Hrow; rewrite -rcons_cons Htab' andbT => /is_row_rconsK /= -> /=. split; last by rewrite /append_nth /=. case: t' Ht' Hn Hdom Htab' => [// | t1 t']. rewrite to_word_cons allLeq_catE => /andP[_ Ht1]. rewrite mem_cat negb_or => /andP[_ Hn] /=. have {Hn}Ht1 : allLtn t1 n. elim: t1 Ht1 Hn => [// | l1 t1 IHt1] /= /andP[Hl1 {}/IHt1 Hrec]. rewrite inE negb_or => /andP[Hl1n /Hrec ->]. by rewrite andbT lt_def Hl1n Hl1. rewrite -rcons_cons; move: (l0 :: t0) => {l0}t0. rewrite !dominate_recE => Hdom _. elim: t1 t0 Ht1 Hdom => [| l1 t1 IHt1] [|l0 t0] //=. by move=> /andP[/ltW]; rewrite leNgt => /negbTE ->. by move=> /andP[_ {}/IHt1 Hrec] /andP[-> /Hrec]. - move=> Hlast /= Hrow Hdom Htab'. rewrite to_word_cons mem_cat cat_uniq allLeq_catE. case: (boolP (n \in to_word t')) => [Hn _ | _ Hn] /andP[Hall Hall0]. + move => /andP[Huniq _] {Hall0 Hlast}. rewrite {}Hrow /=. have {IHt Htab' Hn Hall Huniq} := IHt Htab' Hn Hall Huniq => [] [] -> Happ. split; last by move: Happ; rewrite /append_nth /= => ->. move: Hdom; rewrite andbT {Happ} !dominate_recE. case: t' => [// | t1 t'] /=. case: t1 => [// | l1 t1] /=. case: eqP => //= _. case/lastP: t1 => [// | t1 tl1]. rewrite rcons_nilF belast_rcons /= => /andP[->]/= {l1 l0 t'}. elim: t1 t0 => [// | l1 t1 IHl1] [|l0 t0] //= /andP[->]. exact: IHl1. + exfalso => {IHt Hdom t' Htab' Hall}. case/lastP: t0 Hn Hlast Hrow Hall0 => [/= | t0 tn]. by rewrite inE => /eqP ->; rewrite eq_refl. rewrite orFb -/(is_row (l0 :: _)). rewrite -rcons_cons last_rcons. move: (l0 :: t0) => {l0}t0 /= Hn Htnn /is_rowP Hrow. have Hind := nth_index 0 Hn. move: Hn; rewrite -index_mem size_rcons ltnS => Hsz. have {Hrow} /(Hrow 0) : index n (rcons t0 tn) <= size t0 < size (rcons t0 tn). by rewrite Hsz size_rcons ltnS /=. rewrite Hind nth_rcons ltnn eq_refl {Hind Hsz} => Hn /allLeq_last. by rewrite leNgt lt_def Htnn Hn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau