proposition: Lemma bigcprodEY I r (P : pred I) (H : I -> {group gT}) G : abelian G -> (forall i, P i -> H i \subset G) -> \big[cprod/1]_(i <- r | P i) H i = (\prod_(i <- r | P i) H i)%G.
proof: Proof. move=> cGG sHG; apply/eqP; rewrite !(big_tnth _ _ r). by apply/bigcprodYP=> i j Pi Pj _; rewrite (sub_abelian_cent2 cGG) ?sHG. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)