proposition: Lemma exchange_big_dep : forall (I J : finType) (P : pred I) (Q : I -> pred J) (xQ : pred J) F, (forall i j, P i -> Q i j -> xQ j) -> \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j === \big[*%M/1]_(j | xQ j) \big[*%M/1]_(i | P i && Q i j) F i j.
proof: Proof. move=> I J P Q xQ F PQxQ; pose p u := (u.2, u.1). rewrite -> !pair_big_dep, (reindex_onto (h:=p J I) (h':=p I J)) => [|[//]]. apply eq_big=> [] [j i] //=;try reflexivity; symmetry. by rewrite eq_refl andbC; case: (@andP (P i)) => //= [[]]; exact: PQxQ. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops