proposition: Lemma big_scaleptl' (T : convType) (x : scaled T) : scalept R0 x = Zero -> forall (I : Type) (r : seq I) (P : pred I) (F : I -> R), (forall i : I, 0 <= F i) -> scalept (\sum_(i <- r | P i) F i) x = \ssum_(i <- r | P i) scalept (F i) x.
proof: Proof. move=> H I r P F H'. transitivity (\ssum_(i <- r | P i) (fun r0 : Rnng => scalept r0 x) (mkRnng (H' i))); last reflexivity. rewrite -big_scaleptl ?scalept0 //. congr scalept. transitivity (\sum_(i <- r | P i) mkRnng (H' i)); first reflexivity. apply (big_ind2 (fun x y => x = (Rnng.v y))) => //. by move=> x1 [v Hv] y1 y2 -> ->. 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