proposition: Lemma pair_big : forall (I J : finType) (P : pred I) (Q : pred J) F, \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q j) F i j === \big[*%M/1]_(p | P p.1 && Q p.2) F p.1 p.2.
proof: Proof. move=> *; exact: pair_big_dep. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops