proposition: Lemma yamtab_shift_drop innev maxi sh y : forall res shape, (res, shape) \in yamtab_shift innev maxi sh y -> drop sh res = y.
proof: Proof. Proof using . elim: sh => [//| sh IHsh] /= res shape. by rewrite mem_seq1 => /eqP[-> _]; rewrite drop0. by move=> /flatten_mapP[[rec shrec]] /IHsh Hdrop /mapP[i _ [-> _]]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule