proposition: Lemma mleadc_prod T (r : seq T) (P : pred T) (F : T -> {mpoly R[n]}) : (\prod_(p <- r | P p) F p)@_(\sum_(p <- r | P p) mlead (F p))%MM = \prod_(p <- r | P p) mleadc (F p).
proof: Proof. elim: r => [|p r ih]; first by rewrite !big_nil mcoeff1 eqxx. rewrite !big_cons; case: (P p); rewrite // mleadcMW //. by rewrite ih. by apply/mlead_prod_le. 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