proposition: Lemma LRyamtab_eval inner eval outer tab: is_part inner -> is_part outer -> included inner outer -> is_part eval -> sumn eval = sumn (outer / inner) -> tab \in (LRyamtab_list inner eval outer) -> evalseq (to_word tab) = eval.
proof: Proof. move=> Hinn Hout Hincl Hev Hsumn Htab. apply (included_sumnE Hev (LRyamtab_included Htab)). rewrite Hsumn evalseq_eq_size size_to_word /size_tab. by rewrite (LRyamtab_shape Hinn Hout Hincl Htab). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule