proposition: Lemma big_allpairs I1 I2 (r1 : seq I1) (r2 : seq I2) F : \big[*%M/1]_(i <- [seq (i1, i2) | i1 <- r1, i2 <- r2]) F i = \big[*%M/1]_(i1 <- r1) \big[op/idx]_(i2 <- r2) F (i1, i2).
proof: Proof. exact: big_allpairs_dep. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)