proposition: Lemma bigprodGEgen I r (P : pred I) (F : I -> {set gT}) : (\prod_(i <- r | P i) <<F i>>)%G :=: << \bigcup_(i <- r | P i) F i >>.
proof: Proof. elim/big_rec2: _ => /= [|i A _ _ ->]; first by rewrite gen0. by rewrite joing_idl joing_idr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)