proposition: Lemma LRyamtab_list_skew_tableau0 innev inner outer sh0 row0 : sorted geq (sh0 :: inner) -> is_part (sh0 + size row0 :: outer) -> included inner outer -> size inner = size outer -> is_row row0 -> forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 -> is_skew_tableau (sh0 :: inner) (row0 :: res).
proof: Proof. Proof using . move=> Hinn Hout Hincl Hsize Hrow0 res Hres. have:= LRyamtab_list_shape0 Hinn Hout Hincl Hsize Hres. move: Hinn Hout Hincl Hsize Hrow0 res Hres. elim: outer innev inner sh0 row0 => [/= | out0 out IHout] innev inner sh0 row0 Hinn Hout /= Hincl Hsize Hrow0 res. rewrite mem_seq1 => /eqP -> /=; move: Hsize => /eqP/nilP ->. by move: Hout; rewrite eq_refl Hrow0 !andbT addnC lt0n. case: inner Hinn Hincl Hsize => [// | inn0 inn] Hinn /= /andP[H0 Hincl]. move/eqP; rewrite eqSS => /eqP Hsize. move=> /flatten_mapP[[rshift shrshift]]. move=> /flatten_mapP[[rrow shrrow]] /= Hrow Hshift. move=> /mapP[rec Hrec Hres]; subst res. have Hrshiftrow := yamtab_shift_is_row (yamtab_rows_is_row Hrow) Hshift. have Hrshiftdom := yamtab_shift_dominate (yamtab_rows_dominate Hrow) Hshift. move {Hshift Hrow rrow shrrow}=> /= [Hshift Hshape]. rewrite (part_head_non0 Hout) Hrow0 Hrshiftrow. rewrite Hshift (subnKC H0) (part_head_non0 (is_part_consK Hout)) /=. have Hpart0 : is_part (inn0 + size rshift :: out). have:= is_part_consK Hout => /= /andP[Hhout ->]. by rewrite andbT Hshift (subnKC H0). move/(_ _ _ _ _ (path_sorted Hinn) Hpart0 Hincl Hsize Hrshiftrow _ Hrec Hshape): IHout. move=> {Hrec Hpart0} /= /and3P[_ _ ->]; rewrite andbT. case: (leqP sh0 out0) Hrshiftdom => [_ | /ltnW Hover _]. - exact: skew_dominate_take. - apply skew_dominate_no_overlap. rewrite Hshift leq_subLR. move: Hinn => /= /andP[Hsh0 _]. by rewrite (subnKC Hsh0). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule