proposition: Lemma exchange_big_dep_nat_idem m1 n1 m2 n2 (P : pred nat) (Q : rel nat) (xQ : pred nat) F : (forall i j, m1 <= i < n1 -> m2 <= j < n2 -> P i -> Q i j -> xQ j) -> \big[op/x]_(m1 <= i < n1 | P i) \big[op/x]_(m2 <= j < n2 | Q i j) F i j = \big[op/x]_(m2 <= j < n2 | xQ j) \big[op/x]_(m1 <= i < n1 | P i && Q i j) F i j.
proof: Proof. move=> PQxQ; under eq_bigr do rewrite big_seq_cond. rewrite big_seq_cond /= (exchange_big_dep_idem xQ) => [|i j]; last first. by rewrite !mem_index_iota => /andP[mn_i Pi] /andP[mn_j /PQxQ->]. rewrite 2!(big_seq_cond _ _ _ xQ); apply: eq_bigr => j /andP[-> _] /=. by rewrite [rhs in _ = rhs]big_seq_cond; apply: eq_bigl => i; rewrite -andbA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)