proposition: Lemma cfdot_bigdprod phi psi : '[cfBigdprod phi, cfBigdprod psi] = \prod_(i | P i) '[phi i, psi i].
proof: Proof. apply: canLR (mulKf (neq0CG G)) _; rewrite -(bigdprod_card defG). rewrite (big_morph _ (@natrM _) (erefl _)) -big_split /=. rewrite (eq_bigr _ (fun i _ => mulVKf (neq0CG _) _)) (big_distr_big_dep 1%g) /=. set F := pfamily _ _ _; pose h (f : {ffun I -> gT}) := (\prod_(i | P i) f i)%g. pose is_hK x f := forall f1, (f1 \in F) && (h f1 == x) = (f == f1). have /fin_all_exists[h1 Dh1] x: exists f, x \in G -> is_hK x f. case Gx: (x \in G); last by exists [ffun _ => x]. have [f [Af fK Uf]] := mem_bigdprod defG Gx. exists [ffun i => if P i then f i else 1%g] => _ f1. apply/andP/eqP=> [[/pfamilyP[Pf1 Af1] /eqP Dx] | <-]. by apply/ffunP=> i; rewrite ffunE; case: ifPn => [/Uf-> | /(supportP Pf1)]. split; last by rewrite fK; apply/eqP/eq_bigr=> i Pi; rewrite ffunE Pi. by apply/familyP=> i; rewrite ffunE !unfold_in; case: ifP => //= /Af. rewrite (reindex_onto h h1) /= => [|x /Dh1/(_ (h1 x))]; last first. by rewrite eqxx => /andP[_ /eqP]. apply/eq_big => [f | f /andP[/Dh1<- /andP[/pfamilyP[_ Af] _]]]; last first. by rewrite !cfBigdprodE // rmorph_prod -big_split /=. apply/idP/idP=> [/andP[/Dh1<-] | Ff]; first by rewrite eqxx andbT. have /pfamilyP[_ Af] := Ff; suffices Ghf: h f \in G by rewrite -Dh1 ?Ghf ?Ff /=. by apply/group_prod=> i Pi; rewrite (subsetP (sAG Pi)) ?Af. 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)