proposition: Lemma yam_of_rowpart d y : is_yam_of_eval (rowpartn d) y -> y = ncons d 0%N [::].
proof: Proof. Proof using . rewrite rowpartnE => /andP[Hyam /eqP]. elim: d y Hyam => [// | d IHd] /=. move=> y _; exact: evalseq0. case=> [| y0 y] //= /andP[_ {}/IHd Hrec]. case: y0 => [| y0] /= Heval. * case Heval: (evalseq y) Heval => [| ev0 ev] //=. by move: Heval => /evalseq0 -> [<- /=]. move => [Hev0 Hev]; subst. rewrite {}Hrec // Heval. case: d Heval => [|//] Heval. exfalso; case: y Heval => [// | y0 y] /=. case: (evalseq y) y0 => [| a [| l0 l]] [|[|y0]] //=. * by exfalso; case: (evalseq y) y0 Heval => [| a [| l0 l]] [|y0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools ordcast combclass partition skewpart Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur