proposition: Lemma mem_prodg (I : finType) (P : pred I) (A : I -> {set gT}) c : (forall i, P i -> c i \in A i) -> \prod_(i | P i) c i \in \prod_(i | P i) A i.
proof: Proof. by move=> Ac; apply/prodsgP; exists c. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)