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