proposition: Lemma exchange_big_idem I J rI rJ (P : pred I) (Q : pred J) F : \big[op/x]_(i <- rI | P i) \big[op/x]_(j <- rJ | Q j) F i j = \big[op/x]_(j <- rJ | Q j) \big[op/x]_(i <- rI | P i) F i j.
proof: Proof. rewrite (exchange_big_dep_idem Q) //. by under eq_bigr => i Qi do under eq_bigl do rewrite Qi andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)