proposition: Lemma bigdprod_card I r (P : pred I) E G : \big[dprod/1]_(i <- r | P i) E i = G -> (\prod_(i <- r | P i) #|E i|)%N = #|G|.
proof: Proof. elim/big_rec2: _ G => [G <- | i A B _ IH G defG]; first by rewrite cards1. have [[_ H _ defH] _ _ _] := dprodP defG. by rewrite -(dprod_card defG) (IH H) defH. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)