proposition: Lemma CV_disk_0 (a : nat -> R) : CV_disk a 0.
proof: Proof. exists (Rabs (a O)). apply (is_lim_seq_ext (fun _ => Rabs (a O)) _ (Rabs (a O))). elim => /= [ | n IH]. by rewrite sum_O Rmult_1_r. by rewrite sum_Sn /= Rmult_0_l Rmult_0_r Rabs_R0 /plus /= Rplus_0_r. by apply is_lim_seq_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series