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