proposition: Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N : (forall i, P i -> 0 <= f i) -> (\sum_(N <= i <oo | P i) (x%:E * f i) = x%:E * \sum_(N <= i <oo | P i) f i).
proof: Proof. move=> f0; rewrite -limeMl//; last exact: is_cvg_nneseries. by apply/congr_lim/funext => /= n; rewrite ge0_sume_distrr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau