proposition: Theorem LRcoeffE : LRyam_coeff P1 P2 P = LRcoeff P1 P2 P.
proof: Proof. Proof using Hincl. rewrite /LRyam_coeff -LRcoeffP -(size_map to_word). rewrite -sum1dep_card (eq_bigr (fun y => count_mem y LRyam_list)); first last. by move=> yam Hyam; rewrite LRyam_spec_recip //= inE. rewrite sum_count_mem. rewrite (eq_in_count (a2 := predT)). by rewrite count_predT -(size_map val) subType_seqP // LRyamtab_all. move=> yam /=. rewrite -(mem_map val_inj) subType_seqP ?LRyamtab_all //=. move=> /mapP[tab Htab ->] {yam}. have Hskew := LRyamtab_skew_tableau (intpartnP P1) (intpartnP P) Hincl Htab. have Hshape := LRyamtab_shape (intpartnP P1) (intpartnP P) Hincl Htab. rewrite /is_skew_reshape_tableau /=. have <- : (outer_shape P1 (shape tab)) = P by rewrite Hshape diff_shapeK. rewrite skew_reshapeK //= -(size_map size tab) -/(shape tab) Hshape size_diff_shape. exact: size_included. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule