proposition: Lemma increasing_series (R : numFieldType) (u_ : R ^nat) : (forall n, 0 < u_ n) -> increasing_seq (series u_).
proof: Proof. move=> u_ge0; apply/increasing_seqP => n. by rewrite !seriesEord/= big_ord_recr ltrDl. 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