proposition: Lemma pair_big_dep : forall (I J : finType) (P : pred I) (Q : I -> pred J) F, \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j === \big[*%M/1]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.
proof: Proof. move=> I J P Q F. rewrite -> (partition_big (P:=fun p => P p.1 && Q p.1 p.2) (p:=fun p => p.1) (Q:=P))=> [|j]; last by case/andP. apply eq_bigr=>i Pi. rewrite -> (reindex_onto (h:=pair i) (h':=fun p => p.2)). by apply eq_bigl=> j; rewrite !eqxx [P i]Pi !andbT. by case=> i' j /=; case/andP=> _ /=; move/eqP->. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops