proposition: Lemma prodsgP (I : finType) (P : pred I) (A : I -> {set gT}) x : reflect (exists2 c, forall i, P i -> c i \in A i & x = \prod_(i | P i) c i) (x \in \prod_(i | P i) A i).
proof: Proof. have [r big_r [Ur mem_r] _] := big_enumP P. pose inA c := all (fun i => c i \in A i); rewrite -big_r; set piAx := x \in _. suffices{big_r} IHr: reflect (exists2 c, inA c r & x = \prod_(i <- r) c i) piAx. apply: (iffP IHr) => -[c inAc ->]; do [exists c; last by rewrite big_r]. by move=> i Pi; rewrite (allP inAc) ?mem_r. by apply/allP=> i; rewrite mem_r => /inAc. elim: {P mem_r}r x @piAx Ur => /= [x _ | i r IHr x /andP[r'i /IHr{}IHr]]. by rewrite unlock; apply: (iffP set1P) => [-> | [] //]; exists (fun=> x). rewrite big_cons; apply: (iffP idP) => [|[c /andP[Aci Ac] ->]]; last first. by rewrite big_cons mem_mulg //; apply/IHr=> //; exists c. case/mulsgP=> c_i _ Ac_i /IHr[c /allP-inAcr ->] ->{x}. exists [eta c with i |-> c_i]; rewrite /= ?big_cons eqxx ?Ac_i. by apply/allP=> j rj; rewrite /= ifN ?(memPn r'i) ?inAcr. by congr (_ * _); apply: eq_big_seq => j rj; rewrite ifN ?(memPn r'i). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)