proposition: Lemma yamtab_unique t : is_tableau t -> is_yam (to_word t) -> t = yamtab (shape t).
proof: Proof. elim/last_ind: t => [//= | t tn IHt] /=. rewrite to_word_rcons /= /shape map_rcons yamtab_rcons -/shape => Htab Hyam. move: IHt => /(_ (is_tableau_rconsK Htab) (is_yam_catr Hyam)) Hrec. rewrite -Hrec; congr (rcons t _). have:= is_part_sht Htab. rewrite /shape map_rcons -/shape. move: Hrec; move: (shape t) => sh Ht; subst t. case/lastP: sh Htab Hyam => [| sh sn] /=. move=> /and3P[_ Hrow _]. rewrite /yamtab /= cats0 => /last_yam Hlast _. case: tn Hrow Hlast => [// | l0 tn] /=. elim: tn l0 => [l0 _ /= -> // | l1 t' IHt] /= l0 /andP[Hl0l1 Hpath] Hlast. have {IHt Hpath Hlast} [] := IHt l1 Hpath Hlast => Hl1 <-. by move: Hl0l1; rewrite Hl1 leEnat leqn0 => /eqP ->. rewrite {1}yamtab_rcons -2!cats1 -catA /=. move => /is_tableau_catr /= /and4P[]. case: sn => [// | sn] /= _ _ Hdom /and3P[Hrow Hn2 _]. rewrite to_word_yamtab size_rcons. case/lastP: tn Hrow Hn2 Hdom => [// | tn ln] /= _ Hrow Hdom. rewrite -{1}cats1 -catA cat1s. move=> /is_yam_catr /= /andP[Hpart _] /is_part_rconsK Hp0. move: Hpart; rewrite (evalseq_hyper_yam Hp0) => Hp1. have Hln : ln <= (size sh).+1. elim: sh ln Hp0 Hp1 {Hdom Hrow} => [| s0 sh IHsh] /= ln. case: ln => [//= | ln] _ /= /andP[_ /part_head_non0]. by case: ln. case: ln => [//= | ln]. rewrite ltnS /= => /andP[_ H1] /andP[_ H2]. exact: IHsh. case: tn Hrow Hdom {Hp0 Hp1} => [_ /= | l0 tn]. move=> /dominateP[_ Hdom]; congr [:: _]. apply/eqP; rewrite eqn_leq Hln /=. move/(_ 0 (ltn0Sn _)): Hdom => /=. by rewrite ltEnat. rewrite rcons_cons => Hrow /dominateP[_ Hdom]. move/(_ 0 (ltn0Sn _)): Hdom => /=. rewrite ltEnat => Hl0. elim: tn l0 Hl0 Hrow => [/= | l1 tn /= IHtn] l0 Hl0; rewrite leEnat => /andP[]. move=> Hl0ln _. have {}Hl0 : l0 = (size sh).+1. apply/eqP; rewrite eqn_leq Hl0 andbT. exact: (leq_trans Hl0ln). rewrite Hl0; congr [:: _; _]. apply/eqP; rewrite eqn_leq Hln /=. by rewrite -Hl0. move=> Hl0l1 Hpath. have Hrec := (IHtn l1 (leq_trans Hl0 Hl0l1) Hpath). rewrite -Hrec; congr (_ :: _). apply/eqP; rewrite eqn_leq Hl0 andbT. by move: Hrec => [<- _]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple finfun finset path bigop order) tools partition Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact