proposition: Lemma Cexp_exp_compat : forall a : R, Cexp a = exp a.
proof: Proof. intros a ; unfold exp, Cexp ; destruct (exist_exp a) as (l, H). pose (l1 := sum exp_seq exp_infinite_cv_radius (a +i 0)) ; assert (H1 := sum_sums _ exp_infinite_cv_radius (a +i 0)) ; replace (sum exp_seq exp_infinite_cv_radius (a +i 0)) with l1 in * by reflexivity. rewrite <- Ceq ; simpl. split. apply (Rseq_cv_unique (sum_f_R0 (fun j : nat => (/ INR (fact j) * a ^ j)%R))). apply Rseq_cv_eq_compat with (fun n => Cre (sum_f_C0 (fun j : nat => / INC (fact j) * (a +i 0) ^ j) n)). intro n ; induction n. simpl ; field. rewrite sum_f_C0_simpl, tech5, <- Cre_add_compat, IHn ; apply Rplus_eq_compat_l. rewrite Cre_mul, Cpow_Cim_0, Cpow_Cre_0, Rmult_0_r, Rminus_0_r. rewrite INC_inv_Cre_INR ; [reflexivity | apply fact_neq_0]. apply (Cseq_Rseq_Rseq_equiv _ _) ; apply Pser_Cseqcv_link ; unfold exp_seq in H1 ; apply H1. apply H. apply (Rseq_cv_unique (fun n => Cim (sum_f_C0 (fun j : nat => / INC (fact j) * (a +i 0) ^ j) n))). apply (Cseq_Rseq_Rseq_equiv _ _) ; apply Pser_Cseqcv_link ; unfold exp_seq in H1 ; apply H1. apply (Rseq_cv_eq_compat R0) ; [| apply Rseq_constant_cv]. intro n ; induction n ; unfold Rseq_constant in *. simpl ; field. rewrite sum_f_C0_simpl, <- Cim_add_compat, <- IHn, Cim_mul, Cpow_Cim_0, Cpow_Cre_0, INC_inv_Cim_INR ; [ring | apply fact_neq_0]. 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