proposition: Lemma exchange_big_dep_idem I J rI rJ (P : pred I) (Q : I -> pred J) (xQ : pred J) F : (forall i j, P i -> Q i j -> xQ j) -> \big[op/x]_(i <- rI | P i) \big[op/x]_(j <- rJ | Q i j) F i j = \big[op/x]_(j <- rJ | xQ j) \big[op/x]_(i <- rI | P i && Q i j) F i j.
proof: Proof. move=> PQxQ; pose p u := (u.2, u.1). under [LHS]eq_bigr do rewrite big_tnth; rewrite [LHS]big_tnth. under [RHS]eq_bigr do rewrite big_tnth; rewrite [RHS]big_tnth. rewrite !pair_big_dep_idem (reindex_onto (p _ _) (p _ _)) => [|[]] //=. apply: eq_big => [] [j i] //=; symmetry; rewrite eqxx andbT andb_idl //. by case/andP; apply: PQxQ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)