proposition: Lemma bigdprodYP (I : finType) (P : pred I) (F : I -> {group gT}) : reflect (forall i, P i -> (\prod_(j | P j && (j != i)) F j)%G \subset 'C(F i) :\: (F i)^#) (\big[dprod/1]_(i | P i) F i == (\prod_(i | P i) F i)%G).
proof: Proof. apply: (iffP eqP) => [defG i Pi | dxG]. rewrite !(bigD1 i Pi) /= in defG; have [[_ G' _ defG'] _ _ _] := dprodP defG. by apply/dprodYP; rewrite -defG defG' bigprodGE (bigdprodWY defG'). 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 //]]. apply/dprodYP; apply: subset_trans (dxG i (sQP i Qi)); rewrite !bigprodGE. by apply: genS; apply/bigcupsP=> j /andP[Qj ne_ji]; rewrite (bigcup_max j) ?sQP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)