proposition: Lemma le_psum (F1 F2 : T -> R) : (forall x, 0 <= F1 x <= F2 x) -> summable F2 -> psum F1 <= psum F2.
proof: Proof. move=> le_F smF2; have smF1: summable F1 by apply/(le_summable le_F). rewrite /psum (asboolT smF1) (asboolT smF2); apply/le_sup; first last. + by apply/summable_sup. + by exists 0, fset0; rewrite big_fset0. move=> x [J ->]; apply/downP; exists (\sum_(j : J) `|F2 (val j)|). by exists J. apply/ler_sum=> /= j _; case/andP: (le_F (val j)) => h1 h2. by rewrite !ger0_norm // (le_trans h1 h2). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology