proposition: Lemma mderivwE i p k : msize p <= k -> p^`M(i) = \sum_(m : 'X_{1..n < k}) ((m i)%:R * p@_m) *: 'X_[m - U_(i)].
proof: Proof. pose I : subFinType _ := 'X_{1..n < k}. move=> le_pk; rewrite /mderiv (big_mksub I) /=; first last. by move=> x /msize_mdeg_lt/leq_trans/(_ le_pk). by rewrite msupp_uniq. rewrite big_rmcond //= => j /memN_msupp_eq0 ->. by rewrite mulr0 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