proposition: Lemma scalept_sum (B : finType) (P : pred B) (F : B ->R^+) (x : A) : scalept (\sum_(i | P i) F i) x = \ssum_(b | P b) scalept (F b) x.
proof: Proof. apply: (@proj1 _ (0 <= \sum_(i | P i) F i))%coqR. apply: (big_ind2 (fun y q => scalept q x = y /\ (0 <= q)))%coqR. + by split; [rewrite scale0pt//|exact/Rle_refl]. + move=> _ x2 _ y2 [<- ?] [<- ?]. by rewrite scaleptDl //; split => //; exact: addR_ge0. + by move=> i _; split => //; exact/nneg_f_ge0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist