proposition: Lemma Cexp_0 : Cexp C0 = C1.
proof: Proof. replace C0 with (IRC (IZR 0)) by auto. rewrite Cexp_exp_compat ; rewrite exp_0 ; 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