proposition: Lemma ex_series_Rabs (a : nat -> R) : ex_series (fun n => Rabs (a n)) -> ex_series a.
proof: Proof. move => H. apply: ex_series_Cauchy. apply Cauchy_series_Reals. apply cauchy_abs. apply Cauchy_series_Reals. by apply: Cauchy_ex_series. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy