proposition: Lemma pihomogwE k p : msize p <= k -> pihomog p = \sum_(m : 'X_{1..n < k} | mf m == d) p@_m *: 'X_[m].
proof: Proof. move=> lt_pk; pose I : subFinType _ := 'X_{1..n < k}. rewrite pihomogE (big_mksub_cond I) //=; first last. + by move=> x /msize_mdeg_lt /leq_trans /(_ lt_pk) ->. + by rewrite msupp_uniq. rewrite -big_filter_cond big_rmcond ?big_filter //=. by move=> m /memN_msupp_eq0 ->; rewrite scale0r. 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