proposition: Corollary MN_coeff_recP d (la : 'P_d) : 'p[la] = \sum_(sh : 'P_d) (MN_coeff_fast sh la)%:~R *: 's[sh] :> SF.
proof: Proof. rewrite -[LHS]mul1r -(syms0 _ _ (colpartn 0)). by rewrite syms_prod_sympM; apply eq_bigr => sh _; rewrite colpartnE. 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