proposition: Lemma lreg_prod (T : eqType) (R : ringType) (r : seq T) (P : pred T) (F : T -> R): (forall x, x \in r -> P x -> GRing.lreg (F x)) -> GRing.lreg (\prod_(x <- r | P x) F x).
proof: Proof. elim: r => [|x r ih] h; first by rewrite !big_nil; apply/lreg1. rewrite big_cons; set X := (\prod_(_ <- _ | _) _)%R. have lreg_X: GRing.lreg X by apply/ih=> y ? /h; apply; rewrite mem_behead. by case: ifP => // Px; apply/lregM/lreg_X/h/Px/mem_head. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)