proposition: Lemma nneseries_sum_nat (R : realType) n (f : nat -> nat -> \bar R) : (forall i j, 0 <= f i j) -> \sum_(j <oo) (\sum_(0 <= i < n) f i j) = \sum_(0 <= i < n) (\sum_(j <oo) (f i j)).
proof: Proof. move=> f0; elim: n => [|n IHn]. by rewrite big_geq// eseries0// => i; rewrite big_geq. rewrite big_nat_recr// -IHn/= -nneseriesD//; last by move=> i; rewrite sume_ge0. by apply/congr_lim/funext => m; apply: eq_bigr => i _; rewrite big_nat_recr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau