proposition: Lemma yamtabP sh : is_part sh -> is_tableau (yamtab sh).
proof: Proof. rewrite /yamtab; move: 0. elim: sh => [//= | s0 sh IHsh] i Hpart. have /= Hs0 := part_head_non0 Hpart. apply /and4P; repeat split. - by move: Hs0; apply contra; case s0. - move: Hs0 {Hpart}; case: s0 => [//= | l] _. by elim: l => [//= | l] /= ->; rewrite andbT. - have -> : head [::] (yamtab_rec i.+1 sh) = nseq (head 0 sh) i.+1. by case sh => [//= | l0 l] /=. move: Hpart => /= /andP[Hhead _]. move: Hhead; case: sh {IHsh} => [//= | s1 /= _] Hs. apply /dominateP; split; first by rewrite !size_nseq. move=> j; rewrite size_nseq !nth_nseq => Hj. by rewrite Hj (leq_trans Hj Hs) ltEnat /=. - by move: Hpart => /= /andP[_]; exact: IHsh. 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