proposition: Lemma cfBigdprodEi i (phi : 'CF(A i)) x : P i -> (forall j, P j -> x j \in A j) -> cfBigdprodi phi (\prod_(j | P j) x j)%g = phi (x i).
proof: Proof. have [r big_r [Ur mem_r] _] := big_enumP P => Pi AxP. have:= bigdprodWcp defG; rewrite -!big_r => defGr. have{AxP} [r_i Axr]: i \in r /\ {in r, forall j, x j \in A j}. by split=> [|j]; rewrite mem_r // => /AxP. rewrite (perm_bigcprod defGr Axr (perm_to_rem r_i)) big_cons. rewrite cfDprodEl ?Pi ?cfRes_id ?Axr // big_seq group_prod // => j. rewrite mem_rem_uniq // => /andP[i'j /= r_j]. by apply/mem_gen/bigcupP; exists j; [rewrite -mem_r r_j | apply: Axr]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)