proposition: Lemma LRyamtab_skew_tableau inner eval outer tab : is_part inner -> is_part outer -> included inner outer -> tab \in (LRyamtab_list inner eval outer) -> is_skew_tableau inner tab.
proof: Proof. move=> Hinn Hout Hincl. rewrite /LRyamtab_list LRyamtab_list_pad0 is_skew_tableau_pad0 => Htab. rewrite (LRyamtab_list_size Htab); move: Htab. have {}Hinn : sorted geq (head 1 outer :: (pad 0 (size outer)) inner). 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[-> _] ->. have {}Hout : is_part (head 1 outer + (@size nat) [::] :: outer). by rewrite /= addn0 leqnn Hout. have Hincl0 : included ((pad 0 (size outer)) inner) outer. by rewrite -included_pad0. have Hsize : size ((pad 0 (size outer)) inner) = size outer. rewrite size_cat size_nseq; apply subnKC. exact: size_included. have Hrow : is_row (@nil nat) by []. by move/(LRyamtab_list_skew_tableau0 Hinn Hout Hincl0 Hsize Hrow) => /= /and3P[]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule