proposition: Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) : (forall n, P n -> 0 <= u_ n)%R -> nondecreasing_seq (fun n=> \sum_(0 <= k < n | P k) u_ k)%R.
proof: Proof. move=> u_ge0; apply/nondecreasing_seqP => n. rewrite [in leRHS]big_mkcond [in leRHS]big_nat_recr//=. by rewrite -[in leRHS]big_mkcond/= lerDl; case: ifPn => //; exact: u_ge0. 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