proposition: Lemma count_mem_LRyamtab_list inner eval outer yamtab : is_part inner -> is_part outer -> included inner outer -> is_skew_tableau inner yamtab -> shape yamtab = outer / inner -> is_yam_of_eval eval (to_word yamtab) -> count_mem yamtab (LRyamtab_list inner eval outer) = 1.
proof: Proof. move=> Hinn Hout Hincl. rewrite /LRyamtab_list LRyamtab_list_pad0 is_skew_tableau_pad0 => Htab Hshape Hyam. have Hnil : is_part [::] by []. have {}Hinn : sorted geq (head 1 outer :: (pad 0 (size outer)) inner). have /= := is_part_pad0 (size outer) Hinn. case: inner Hincl {Hinn Hout Htab Hshape} => [// | inn0 inn] /=. + by rewrite subn0; case outer. + by case: outer => [// | out0 out] /= /andP[-> _] ->. have Hsztab : size yamtab = size outer. by rewrite -(size_diff_shape inner outer) -Hshape size_map. have {}Hout : is_part ((head 1 outer + @size nat [::]) :: outer_shape ((pad 0 (size outer)) inner) (shape yamtab)). rewrite [size [::]]/= addn0 -Hsztab -(size_map size yamtab) -/(shape _). rewrite outer_shape_pad0 Hshape (diff_shapeK Hincl). case: outer Hout {Hincl Hshape Hinn Hsztab} => [//= | s0 s] /= ->. by rewrite leqnn. have Hsize : size ((pad 0 (size outer)) inner) = size yamtab. rewrite size_cat size_nseq subnKC; last exact: size_included. by rewrite -(size_diff_shape inner outer) -Hshape size_map. have Hskew : is_skew_tableau (head 1 outer :: (pad 0 (size outer)) inner) ([::] :: yamtab). move: Htab; rewrite Hsztab /= => ->; rewrite andbT (part_head_non0 Hout) /=. case: outer Hincl Hshape Hsztab {Hinn Hout Hsize} => [|out0 out] /=. by case: inner => [ _ _ /eqP/nilP ->| in0 inn] //=. case: inner => [_ | in0 inn] //=. case: yamtab {Hyam} => [ | yam0 yam] //= [Hyam _] _. by rewrite subn0; rewrite /skew_dominate -Hyam drop_size. move=> /andP[Hincl _]. case: yamtab {Hyam}=> [ | yam0 yam] //= [Hyam _] _. by rewrite /skew_dominate -Hyam drop_size. have {2}-> : outer = outer_shape ((pad 0 (size outer)) inner) (shape yamtab). by rewrite Hshape -(size_diff_shape inner outer) outer_shape_pad0 (diff_shapeK Hincl). exact: LRyamtab_list_countE Hnil Hinn Hout Hsize Hskew (skew_nil_yamE Hyam). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule