proposition: Lemma msupp_sumX (r : seq 'X_{1..n}) (f : 'X_{1..n} -> R) : uniq r -> {in r, forall m, f m != 0} -> perm_eq (msupp (\sum_(m <- r) (f m) *: 'X_[m])) r.
proof: Proof. move=> uq_r h; set F := fun m => (f m *: 'X_[m] : {mpoly R[n]}). have msFm m: m \in r -> msupp (f m *: 'X_[m]) = [:: m]. by move=> m_in_r; rewrite msuppMCX // h. rewrite (permPl (msupp_sum xpredT _ _)) //. move/eq_in_map: msFm; rewrite filter_predT=> ->. set s := flatten _; have ->: s = r => //. by rewrite {}/s; elim: {uq_r h} r=> //= m r ->. move=> m1 m2 /h nz_fm1 /h nz_fm2 nz_m1m2 m /=. rewrite !msuppMCX // !mem_seq1; case: eqP=> //= ->. by rewrite (negbTE nz_m1m2). 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