proposition: Lemma pair_big_dep_cond (A : {fset I}) (B : I -> {fset J}) (P : pred I) (Q : I -> pred J) (F : I -> J -> R) : \big[op/idx]_(i <- A | P i) \big[op/idx]_(j <- B i | Q i j) F i j = \big[op/idx]_(p <- [fset ((i, j) : I * J) | i in [fset i in A | P i], j in [fset j in B i | Q i j]]) F p.1 p.2.
proof: Proof. rewrite big_imfset2 //=; last by move=> [??] [??] _ _ /= [-> ->]. by rewrite big_fset /=; apply: eq_bigr => i _; rewrite big_fset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)