proposition: Lemma series_le_cvg (R : realType) (u_ v_ : R ^nat) : (forall n, 0 <= u_ n) -> (forall n, 0 <= v_ n) -> (forall n, u_ n <= v_ n) -> cvgn (series v_) -> cvgn (series u_).
proof: Proof. move=> u_ge0 v_ge0 le_uv /cvg_seq_bounded/bounded_fun_has_ubound[M v_M]. apply: nondecreasing_is_cvgn; first exact: nondecreasing_series. exists M => _ [n _ <-]. by apply: le_trans (v_M (series v_ n) _); [apply: ler_sum | exists n]. 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