proposition: Lemma big_pair_dep (P : pred I) (Q : pred (I * J)) (F : I * J -> R) : \big[op/idx]_(p | P p.1 && Q p) F p = \big[op/idx]_(i | P i) \big[op/idx]_(j | Q (i, j)) F (i, j).
proof: Proof. by rewrite pair_big_dep; apply: eq_big => -[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)