proposition: Lemma group_prod I r (P : pred I) F : (forall i, P i -> F i \in G) -> \prod_(i <- r | P i) F i \in G.
proof: Proof. by move=> G_P; elim/big_ind: _ => //; apply: groupM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)