proposition: Lemma CV_disk_le (a : nat -> R) (r1 r2 : R) : Rabs r1 <= Rabs r2 -> CV_disk a r2 -> CV_disk a r1.
proof: Proof. move => H. apply @ex_series_le => n. rewrite /norm /= /abs /= Rabs_Rabsolu. rewrite ?Rabs_mult ; apply Rmult_le_compat_l. by apply Rabs_pos. rewrite -?RPow_abs ; apply pow_incr ; split. by apply Rabs_pos. by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series