proposition: Lemma LRyamtab_shape inner eval outer tab : is_part inner -> is_part outer -> included inner outer -> tab \in (LRyamtab_list inner eval outer) -> shape tab = outer / inner.
proof: Proof. move=> Hinn Hout Hincl. rewrite /LRyamtab_list LRyamtab_list_pad0 -diff_shape_pad0. move => /LRyamtab_list_shape0; apply => //=. - have /= := is_part_pad0 (size outer) Hinn. case: inner Hincl {Hinn Hout} => [// | inn0 inn] /=. + by rewrite subn0; case outer. + by case: outer => [// | out0 out] /= /andP[-> _] ->. - by rewrite addn0 leqnn Hout. - by rewrite -included_pad0. - rewrite size_cat size_nseq; apply subnKC. exact: size_included. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule