proposition: Lemma exchange_big : forall (I J : finType) (P : pred I) (Q : pred J) F, \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q j) F i j === \big[*%M/1]_(j | Q j) \big[*%M/1]_(i | P i) F i j.
proof: Proof. move=> I J P Q F; rewrite -> (exchange_big_dep (Q:=fun i j => Q j) (xQ:=Q))=> //. by apply eq_bigr=> i /= Qi; apply eq_bigl=> j; rewrite [Q i]Qi andbT. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops