proposition: Lemma pihomog_partitionE k p : mfsize p <= k -> p = \sum_(d < k) pihomog d p.
proof: Proof. move=> h; rewrite (exchange_big_dep predT) //= {1}[p]mpolyE. apply/eq_bigr => m _; rewrite -scaler_sumr. case: (ssrnat.leqP k (mf m)) => [|lt_mk]. move/(leq_trans h)/mmeasure_mnm_ge/memN_msupp_eq0. by move=> ->; by rewrite !scale0r. rewrite (eq_bigl (fun i : 'I_k => i == Ordinal lt_mk)). by rewrite big_pred1_eq. by move=> i /=; rewrite eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg