proposition: Lemma bigcprod_coprime_dprod (I : finType) (P : pred I) (A : I -> {set gT}) G : \big[cprod/1]_(i | P i) A i = G -> (forall i j, P i -> P j -> i != j -> coprime #|A i| #|A j|) -> \big[dprod/1]_(i | P i) A i = G.
proof: Proof. move=> defG coA; set Q := P in defG *; have sQP: subpred Q P by []. have [m leQm] := ubnP #|Q|; elim: m => // m IHm in (Q) leQm G defG sQP *. have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0 in defG *. move: defG; rewrite !(bigD1 i Qi) /= => /cprodP[[Hi Gi defAi defGi] <-]. rewrite defAi defGi => cHGi. have{} defGi: \big[dprod/1]_(j | Q j && (j != i)) A j = Gi. by apply: IHm => [||j /andP[/sQP]] //; rewrite (cardD1x Qi) in leQm. rewrite defGi dprodE // coprime_TIg // -defAi -(bigdprod_card defGi). elim/big_rec: _ => [|j n /andP[neq_ji Qj] IHn]; first exact: coprimen1. by rewrite coprimeMr coprime_sym coA ?sQP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)