proposition: Corollary MN_coeff_rec_homogP d (la : 'P_d) : 'hp[la] = \sum_(sh : 'P_d) (MN_coeff_fast sh la)%:~R *: 'hs[sh] :> HSF.
proof: Proof. apply val_inj => /=; apply val_inj => /=. have /= := congr1 val (MN_coeff_recP la); rewrite /prod_symp => ->. by rewrite !raddf_sum. 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