proposition: Lemma LRyamtabP tab : tab \in (LRyamtab_list P1 P2 P) -> is_yam_of_eval P2 (to_word tab).
proof: Proof. Proof using Hincl. rewrite /is_yam_of_eval => Htab; apply /andP; split. - exact: LRyamtab_yam Htab. - rewrite (LRyamtab_eval (intpartnP P1) (intpartnP P) Hincl (intpartnP P2) _ Htab) //=. by rewrite (sumn_diff_shape Hincl) !sumn_intpartn addKn. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule