proposition: Lemma nneseries_interchange (R : realType) (a : nat -> nat -> \bar R) (P Q : pred nat) : (forall i j, 0 <= a i j) -> \sum_(i <oo | P i) \sum_(j <oo | Q j) a i j = \sum_(j <oo | Q j) \sum_(i <oo | P i) a i j.
proof: Proof. move=> a0; rewrite !nneseries_esum_prod//. rewrite (reindex_esum (Q `*` P) _ (fun x => (x.2, x.1)))//; split=> //=. by move=> [i j] [/=]. by move=> [i1 i2] [j1 j2] /= _ _ [] -> ->. by move=> [i1 i2] [Pi1 Qi2] /=; exists (i2, i1). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun