proposition: Lemma mderivmwE k m p : msize p <= k -> p^`M[m] = \sum_(m' : 'X_{1..n < k}) (p@_m' * (\prod_(i < n) (m' i)^_(m i))%:R *: 'X_[m'-m]).
proof: Proof. move=> lt_pk; pose P (m : 'X_{1..n < k}) := (val m) \in msupp p. rewrite (bigID P) {}/P /= addrC big1 ?add0r; last first. by move=> m' /memN_msupp_eq0=> ->; rewrite mul0r scale0r. rewrite mderivmE (big_mksub 'X_{1..n < k}) //=; first exact/msupp_uniq. by move=> m' /msize_mdeg_lt /leq_trans; apply. 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