proposition: Corollary MN_coeffE d (la mu : 'P_d) : MN_coeff_fast la mu = MN_coeff la mu.
proof: Proof. pose HSF := {homsym rat[(sumn mu).+1 , d]}. pose Pval i := (@enum_val _ xpredT i : 'P_d). have : \sum_i (MN_coeff_rec (Pval i) [::] mu)%:~R *: 'hs`_i = \sum_i (MN_coeff (Pval i) mu )%:~R *: 'hs`_i :> HSF. rewrite !(reindex _ (onW_bij _ (@enum_rank_bij 'P_d))) /=. under [LHS]eq_bigr do rewrite /Pval symbsE enum_rankK. under [RHS]eq_bigr do rewrite /Pval symbsE enum_rankK. by rewrite -[LHS]MN_coeff_rec_homogP -[RHS]MN_coeff_homogP. move/(congr1 (coord 'hs (enum_rank la))) => /eqP. have free_hs : free ('hs : seq HSF) by apply: symbs_free; rewrite sumn_intpartn. by rewrite !coord_sum_free // {}/Pval enum_rankK => /eqP/intr_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint perm fingroup tuple vector rat) mathcomp(ssrcomplements freeg mpoly monalg) sorted tools ordtype permuted partition skewpart antisym Schur_mpoly Schur_altdef sympoly homogsym