proposition: Lemma bigcprodYP (I : finType) (P : pred I) (H : I -> {group gT}) : reflect (forall i j, P i -> P j -> i != j -> H i \subset 'C(H j)) (\big[cprod/1]_(i | P i) H i == (\prod_(i | P i) H i)%G).
proof: Proof. apply: (iffP eqP) => [defG i j Pi Pj neq_ij | cHH]. rewrite (bigD1 j) // (bigD1 i) /= ?cprodA in defG; last exact/andP. by case/cprodP: defG => [[K _ /cprodP[//]]]. set Q := P; have sQP: subpred Q P by []; have [n leQn] := ubnP #|Q|. elim: n => // n IHn in (Q) leQn sQP *. have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0. rewrite (cardD1x Qi) add1n ltnS !(bigD1 i Qi) /= in leQn *. rewrite {}IHn {n leQn}// => [|j /andP[/sQP //]]. rewrite bigprodGE cprodEY // gen_subG; apply/bigcupsP=> j /andP[neq_ji Qj]. by rewrite cHH ?sQP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)