proposition: Theorem LRyam_coeff_rowpart (P1 : 'P_d1) (P : 'P_(d1 + d2)) : included P1 P -> LRyam_coeff P1 (rowpartn d2) P = hb_strip P1 P.
proof: Proof. Proof using . rewrite /LRyam_coeff /LRyam_set => Hincl. rewrite /is_skew_reshape_tableau. set LRset := (X in #|pred_of_set X|). case: (boolP (hb_strip P1 P)) => Hstrip /=. - suff -> : LRset = [set yamrow] by rewrite cards1. apply setP => y; rewrite !inE {LRset}. case: y => y Hy /=. have -> : (YamEval Hy == yamrow) = (y == (ncons d2 0%N [::])). apply/idP/idP => /eqP Heq. + by rewrite -[y]/(val (YamEval Hy)) Heq. + apply/eqP; exact: val_inj. move: Hy => /= /yam_of_rowpart ->. rewrite eq_refl; move: Hstrip. rewrite -(hb_strip_rowE (intpartnP _) (intpartnP _) (u := (ncons d2 0%N [::]))); first last. + rewrite size_ncons /= addn0 (sumn_diff_shape_intpartE (rowpartn d2)) //=. by rewrite rowpartnE; case: d2 => [// | d] /=; rewrite addn0. + exact: is_row_yamrow. by move=> /andP[]. - suff -> : LRset = set0 by rewrite cards0. apply/eqP; rewrite -subset0. apply/subsetP => y; rewrite in_set0 inE => Hskew. move: Hstrip. rewrite -(hb_strip_rowE (intpartnP _) (intpartnP _) (u := y)); first last. + rewrite -evalseq_eq_size eval_yameval. by rewrite (sumn_diff_shape_intpartE (rowpartn d2)). + case: y {Hskew} => y /= Hy. suff -> : y = ncons d2 0%N [::] by exact: is_row_yamrow. exact: yam_of_rowpart. by rewrite Hincl Hskew. 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