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