proposition: Lemma Cexp_abs_cv : forall z, {l | Cser_abs_cv (gt_pser exp_seq z) l}.
proof: Proof. intro z ; assert (z_bd : Cnorm z < Cnorm z + 1) by intuition ; destruct (Cpser_abel2_prelim _ _ (exp_infinite_cv_radius (Cnorm z + 1)%R) _ z_bd) as [l Hl]. unfold Cpser_norm in Hl. exists (Cre l) ; unfold Cser_abs_cv. apply Rseq_cv_eq_compat with (fun n => Cre (sum_f_C0 (fun n : nat => Cnorm (gt_pser exp_seq z n)) n)). intro n ; rewrite <- sum_f_C0_Cre_compat ; simpl ; reflexivity. apply Cseq_cv_re_compat. auto. Qed.
imports: Lia Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_usual_facts Rtactic MyRIneq Cprop_base Csequence Csequence_facts Cpser_def Cpser_base_facts Cpser_facts Cseries Cseries_facts Cdefinitions Canalysis_def