proposition: Lemma ex_series_le {K : AbsRing} {V : CompleteNormedModule K} (a : nat -> V) (b : nat -> R) : (forall n : nat, norm (a n) <= b n) -> ex_series b -> ex_series a.
proof: Proof. move => H Hb. apply (Cauchy_ex_series (V := R_CompleteNormedModule)) in Hb. apply ex_series_Cauchy. move => e. case (Hb e) => {Hb} N Hb. exists N => n m Hn Hm. eapply Rle_lt_trans, (Hb _ _ Hn Hm) => //. eapply Rle_trans. apply norm_sum_n_m. apply Rle_trans with (sum_n_m b n m). by apply sum_n_m_le. right. assert (forall n, 0 <= b n). intros k. eapply Rle_trans, H. by apply norm_ge_0. clear -H0. apply sym_eq, Rabs_pos_eq. elim: n m b H0 => /= [ | n IH] m b Hb. elim: m => /= [ | m IH]. rewrite sum_n_n. by apply Hb. rewrite sum_n_Sm. by apply Rplus_le_le_0_compat. by apply Nat.le_0_l. case: m => /= [ | m]. by apply Rle_refl. rewrite -sum_n_m_S. apply IH => k. by apply Hb. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy