proposition: Theorem LRyam_coeff_colpartn (P1 : 'P_d1) (P : 'P_(d1 + d2)) : included P1 P -> LRyam_coeff P1 (colpartn d2) P = vb_strip P1 P.
proof: Proof. Proof using . move=> Hincl. have Hinclc : included (conj_intpartn P1) (conj_intpartn P). exact: included_conj_part. rewrite -conj_rowpartn -{1}(conj_intpartnK P1) -{1}(conj_intpartnK P). rewrite -LRyam_coeffE; last by rewrite !conj_intpartnK. rewrite -LRtab_coeff_conj (LRyam_coeffE _ Hinclc) (LRyam_coeff_rowpart Hinclc). by rewrite /= hb_strip_conjE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools ordcast combclass partition skewpart Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur