proposition: Lemma exchange_big_nat : forall m1 n1 m2 n2 (P Q : pred nat) F, \big[*%M/1]_(m1 <= i < n1 | P i) \big[*%M/1]_(m2 <= j < n2 | Q j) F i j === \big[*%M/1]_(m2 <= j < n2 | Q j) \big[*%M/1]_(m1 <= i < n1 | P i) F i j.
proof: Proof. move=> m1 n1 m2 n2 P Q F. rewrite -> (exchange_big_dep_nat (P:=P) (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