proposition: Lemma yamtab_shiftP innev maxi sh row shrow : is_skew_yam innev shrow row -> forall res shape, (res, shape) \in yamtab_shift shrow maxi sh row -> is_skew_yam innev shape res.
proof: Proof. Proof using . elim: sh row innev => [| sh IHsh] /= row innev Hrow res shres. by rewrite mem_seq1 => /eqP[-> ->]. move/flatten_mapP => [[rec shrec]] /(IHsh row innev Hrow) {IHsh} 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