proposition: Lemma yamtab_shift_dominate innev maxi sh row y : dominate y row -> forall res shape, (res, shape) \in yamtab_shift innev maxi sh y -> skew_dominate sh res row.
proof: Proof. Proof using . rewrite -skew_dominate0. elim: sh innev y => [// | sh IHsh] /= innev y Hdom res shape. by rewrite mem_seq1 => /eqP[->]. move/flatten_mapP => [[rec shrec]] /(IHsh _ _ Hdom){IHsh Hdom}Hrec. move/mapP => [i Hi [-> _]]. exact: skew_dominate_consl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule