proposition: Lemma msupp_sum (T : eqType) (r : seq T) (P : pred T) (F : T -> {mpoly R[n]}) : uniq r -> {in r &, forall x y, x != y -> [predI (msupp (F x)) & (msupp (F y))] =1 xpred0} -> perm_eq (msupp (\sum_(i <- r | P i) F i)) (flatten [seq msupp (F i) | i <- r & P i]).
proof: Proof. elim: r => /= [|x r ih]; first by rewrite !big_nil msupp0. case/andP=> x_notin_r uq_r h; rewrite !big_cons /=. case: (P x); last apply/ih=> //; last first. by move=> y1 y2 y1_in_r y2_in_r; apply/h; rewrite 1?mem_behead. move/(_ uq_r): ih; rewrite -(perm_cat2l (msupp (F x))) => h'. rewrite -(permPr (h' _)); first apply/msuppD. move=> m /=; case: (boolP (m \in _))=> //= m_in_Fx. apply/negP=> /msupp_sum_le /flattenP[/= ms] /mapP[y]. rewrite mem_filter => /andP[_ y_in_r] ->. have /= := h x y _ _ _ m; rewrite m_in_Fx=> /= -> //. by rewrite mem_head. by rewrite mem_behead. by move/memPnC: x_notin_r => /(_ _ y_in_r). by move=> y1 y2 y1_in_r y2_in_r; apply/h; rewrite 1?mem_behead. 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