proposition: Lemma bigprodGE I r (P : pred I) (F : I -> {group gT}) : (\prod_(i <- r | P i) F i)%G :=: << \bigcup_(i <- r | P i) F i >>.
proof: Proof. rewrite -bigprodGEgen /=; apply: congr_group. by apply: eq_bigr => i _; rewrite genGidG. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)