proposition: Lemma bigcprod_card_dprod I r (P : pred I) (A : I -> {set gT}) G : \big[cprod/1]_(i <- r | P i) A i = G -> \prod_(i <- r | P i) #|A i| <= #|G| -> \big[dprod/1]_(i <- r | P i) A i = G.
proof: Proof. elim: r G => [|i r IHr]; rewrite !(big_nil, big_cons) //; case: ifP => _ // G. case/cprodP=> [[K H -> defH]]; rewrite defH => <- cKH leKH_G. have /implyP := leq_trans leKH_G (dvdn_leq _ (dvdn_cardMg K H)). rewrite muln_gt0 leq_pmul2l !cardG_gt0 //= => /(IHr H defH){}defH. by rewrite defH dprodE // cardMg_TI // -(bigdprod_card defH). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)