proposition: Lemma esum_sum [R : realType] [T1 T2 : choiceType] (I : set T1) (r : seq T2) (P : pred T2) (a : T1 -> T2 -> \bar R) : (forall i j, I i -> P j -> 0 <= a i j) -> \esum_(i in I) \sum_(j <- r | P j) a i j = \sum_(j <- r | P j) \esum_(i in I) a i j.
proof: Proof. move=> a_ge0; elim: r => [|j r IHr]; rewrite ?(big_nil, big_cons)// -?IHr. by rewrite esum1// => i; rewrite big_nil. case: (boolP (P j)) => Pj; last first. by apply: eq_esum => i Ii; rewrite big_cons (negPf Pj). have aj_ge0 i : I i -> a i j >= 0 by move=> ?; apply: a_ge0. rewrite -esumD//; last by move=> i Ii; apply: sume_ge0 => *; apply: a_ge0. by apply: eq_esum => i Ii; rewrite big_cons Pj. 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