proposition: Lemma msupp_sum_le (T : Type) (F : T -> {mpoly R[n]}) P (r : seq T) : {subset 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. rewrite !big_cons; case: (P x)=> // m /msuppD_le. by rewrite !mem_cat => /orP [->//|] /ih ->; rewrite orbT. 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