proposition: Lemma psumD S1 S2 : (forall x, 0 <= S1 x) -> (forall x, 0 <= S2 x) -> summable S1 -> summable S2 -> psum (S1 \+ S2) = (psum S1 + psum S2).
proof: Proof. move=> ge0_S1 ge0_S2 smS1 smS2; have smD := summableD smS1 smS2. have ge0D: forall x, 0 <= S1 x + S2 x by move=> x; rewrite addr_ge0. rewrite !psumE // (rwP eqP) eq_le -(rwP andP); split. apply/sup_le_ub. + by exists 0, fset0; rewrite big_fset0. apply/ubP=> _ [J ->]; rewrite big_split /=. apply/lerD; rewrite -psumE 1?(le_trans _ (gerfin_psum J _)) //. + by apply/ler_sum=> j _ /=; apply/ler_norm. + by apply/ler_sum=> j _ /=; apply/ler_norm. rewrite -lerBrDr; apply/sup_le_ub. + by exists 0, fset0; rewrite big_fset0. apply/ubP=> _ [J1 ->]; rewrite lerBrDr addrC. rewrite -lerBrDr; apply/sup_le_ub. + by exists 0, fset0; rewrite big_fset0. apply/ubP=> _ [J2 ->]; rewrite lerBrDr addrC. pose J := J1 `|` J2; rewrite -psumE ?(le_trans _ (gerfin_psum J _)) //. pose D := \sum_(j : J) (S1 (val j) + S2 (val j)). apply/(@le_trans _ _ D); last by apply/ler_sum=> i _; apply/ler_norm. rewrite /D big_split /=; apply/lerD; apply/big_fset_subset=> //. + by apply/fsubsetP/fsubsetUl. + by apply/fsubsetP/fsubsetUr. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology