proposition: Lemma __admitted__psumB S1 S2 : (forall x, 0 <= S2 x <= S1 x) -> summable S1 -> psum (S1 \- S2) = (psum S1 - psum S2).
proof: Proof. Proof using Type. Admitted. Lemma psumZ S c : 0 <= c -> psum (c \*o S) = c * psum S. Proof. rewrite le_eqVlt => /orP[/eqP<-|gt0_c]. by rewrite mul0r psum_eq0 // => x /=; rewrite mul0r. case/asboolP: (summable S) => [smS|NsmS]; last first. rewrite !psum_out ?mulr0 // => smZ; apply/NsmS. move/(summableZ c^-1): smZ; apply/eq_summable=> x /=. by rewrite mulKf // gt_eqF. have smZ := summableZ c smS; rewrite (rwP eqP) eq_le. apply/andP; split; first rewrite {1}/psum asboolT //. apply/sup_le_ub. + by exists 0, fset0; rewrite big_fset0. apply/ubP=> _ [J ->]; rewrite -ler_pdivrMl //. rewrite mulr_sumr (le_trans _ (gerfin_psum J _)) //. apply/ler_sum=> /= j _; rewrite normrM. by rewrite gtr0_norm // mulKf ?gt_eqF. rewrite -ler_pdivlMl // {1}/psum asboolT //; apply/sup_le_ub. + by exists 0, fset0; rewrite big_fset0. apply/ubP=> _ [J ->]; rewrite ler_pdivlMl //. rewrite mulr_sumr; apply/(le_trans _ (gerfin_psum J _))=> //. by apply/ler_sum=> /= j _; rewrite normrM (gtr0_norm gt0_c). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology