proposition: Lemma LRyamtab_list_shape0 innev inner outer sh0 row0 : sorted geq (sh0 :: inner) -> is_part (sh0 + size row0 :: outer) -> included inner outer -> size inner = size outer -> forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 -> shape res = outer / inner.
proof: Proof. Proof using . elim: outer innev inner sh0 row0 => [// | out0 out IHout] innev inner sh0 row0 Hinn Hout /= Hincl Hsize res. by rewrite mem_seq1 => /eqP -> /=; move: Hsize => /eqP/nilP ->. 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 ->] /= {res}. have {}Hshift : size rshift = out0 - inn0. rewrite (yamtab_shift_size Hshift) {Hshift}. move: Hout => /= /andP[Hout0 _]. move: Hinn => /= /andP[Hinn0 _]. move: Hrow => /yamtab_rows_size ->. rewrite !size_takel ?leq_subLR //. rewrite /minn; case: ltnP; last rewrite /leq => /eqP ->. + move/ltnW => H1. by rewrite addnC (addnBA _ Hinn0) (subnK H1). + by rewrite addn0. rewrite Hshift; congr (_ :: _). rewrite (IHout _ _ _ _ (path_sorted Hinn) _ _ _ _ Hrec) {IHout Hrec} //=. rewrite Hshift (subnKC H0) -/(is_part (out0 :: out)). exact (is_part_consK Hout). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule