proposition: Theorem MN_coeffP_int d (la : 'P_d) : 'p[la] = \sum_(sh : 'P_d) MN_coeff sh la *: 's[sh] :> {sympoly int[n]}.
proof: Proof. rewrite /prod_symp /prod_gen. case: la => la /= /andP[/eqP<-{d} /in_part_non0]. elim: la => [/= | l0 la IHla] Hall. rewrite big_nil (big_pred1 (rowpartn 0)) ?scale1r ?syms0 //. by move=> i /=; rewrite intpartn0 eqxx. rewrite big_cons {}IHla; first last. by move=> i iinla; apply: Hall; rewrite inE {}iinla orbT. under [RHS]eq_bigr do rewrite MN_coeff_consE. rewrite mulr_sumr. have {Hall} l0n0 : l0 != 0%N by apply: Hall; rewrite inE eqxx. under eq_bigr do rewrite mulrC -scalerAl syms_sympM // scaler_sumr. rewrite (exchange_big_dep xpredT) //=; apply: eq_bigr => mu _. rewrite scaler_suml; apply eq_bigr => nu _. by rewrite scalerA. 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