proposition: Lemma mem_bigdprod (I : finType) (P : pred I) F G x : \big[dprod/1]_(i | P i) F i = G -> x \in G -> exists c, [/\ forall i, P i -> c i \in F i, x = \prod_(i | P i) c i & forall e, (forall i, P i -> e i \in F i) -> x = \prod_(i | P i) e i -> forall i, P i -> e i = c i].
proof: Proof. move=> defG; rewrite -(bigdprodW defG) => /prodsgP[c Fc ->]. have [r big_r [_ mem_r] _] := big_enumP P. exists c; split=> // e Fe eq_ce i Pi; rewrite -!{}big_r in defG eq_ce. have{Pi}: i \in r by rewrite mem_r. have{mem_r}: all P r by apply/allP=> j; rewrite mem_r. elim: r G defG eq_ce => // j r IHr G. rewrite !big_cons inE /= => /dprodP[[K H defK defH] _ _]. rewrite defK defH => tiFjH eq_ce /andP[Pj Pr]. suffices{i IHr} eq_cej: c j = e j. case/predU1P=> [-> //|]; apply: IHr defH _ Pr. by apply: (mulgI (c j)); rewrite eq_ce eq_cej. rewrite !(big_nth j) !big_mkord in defH eq_ce. move/(congr1 (divgr K H)): eq_ce; move/bigdprodW: defH => defH. move/(all_nthP j) in Pr. by rewrite !divgrMid // -?defK -?defH ?mem_prodg // => *; rewrite ?Fc ?Fe ?Pr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)