proposition: Lemma yamtab_rows_included innev row : included innev outev -> forall res shape, (res, shape) \in yamtab_rows innev row -> included shape outev.
proof: Proof. Proof using . elim: row innev => [| r0 tlr IHrow] /= innev Hincl res shres. by rewrite mem_seq1 => /eqP[_ ->]. move/flatten_mapP => [[rec shrec]] /(IHrow innev Hincl) {IHrow} Hrec. move/mapP => [i Hi [_ ->]]. exact: (one_letter_included Hrec Hi). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule