proposition: Lemma sumn_partm m : sumn (partm m) = mdeg m.
proof: Proof. rewrite sumnE. wlog: m / m \is dominant. move=> Hdom; have Hperm := partm_permK m. rewrite /mdeg (perm_big _ Hperm) /= -/(mdeg _). have /Hdom <- := mpart_is_dominant (intpartP (partm m)). by rewrite mpartK // size_partm. move/is_dominant_partm ->. symmetry; rewrite big_filter /mdeg. by rewrite (bigID (fun i => i == 0)) /= big1 ?add0n // => i /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition