proposition: Lemma mlead_prod_proper : (forall x, x \in r -> P x -> GRing.lreg (mleadc (F x))) -> mlead (\prod_(p <- r | P p) F p) = (\sum_(p <- r | P p) mlead (F p))%MM.
proof: Proof. pose Q (s : seq T) := forall x, x \in s -> P x -> GRing.lreg (mleadc (F x)). rewrite -/(Q r); elim: r => [|x s ih] h; first by rewrite !big_nil mleadC. have lreg_s: Q s. by move=> y y_in_s; apply: (h y); rewrite mem_behead. rewrite !big_cons; case: (boolP (P x))=> Px; last exact/ih. have lreg_x := (h x (mem_head _ _) Px). rewrite mleadM_proper; first by rewrite ih. by rewrite mulrI_eq0 ?ih // mleadc_prod; apply/lreg_neq0/lreg_prod. 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