proposition: Lemma LRyamtab_list_included innev inner outer sh0 row0 y : included innev outev -> is_yam_of_eval innev y -> forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 -> included (evalseq (to_word res ++ y)) outev.
proof: Proof. Proof using . elim: outer innev inner sh0 row0 y => [// | out0 out IHout] /= innev inner sh0 row0 y Hincl Hy res. rewrite mem_seq1 => /eqP -> /=. by move: Hy; rewrite /is_yam_of_eval => /andP[Hyam /eqP ->]. move=> /flatten_mapP[[rshift shrshift]]. move=> /flatten_mapP[[rrow shrrow]] /= Hrow Hshift. move=> /mapP[rec Hrec ->] {res}; rewrite to_word_cons -catA. have Hshshift := yamtab_shiftP (yamtab_rowsP Hrow) Hshift Hy. move: Hrow => /(yamtab_rows_included Hincl)/yamtab_shift_included/(_ _ _ Hshift). move/IHout => H. exact: (H _ _ _ _ Hshshift _ Hrec). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule