proposition: Lemma Cexp_mult : forall a n, Cexp (INC n * a) = (Cexp a) ^ n.
proof: Proof. intros a n ; induction n. simpl ; rewrite Cmult_0_l ; apply Cexp_0. rewrite S_INC, Cpow_S, Cmult_add_distr_r, Cmult_1_l, Cexp_add, IHn ; ring. 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