proposition: Lemma C_infty_exp : C_infty exp.
proof: Proof. intro n ; induction n. constructor ; apply derivable_continuous ; apply derivable_exp. apply C_S with (derivable_exp) ; apply C_ext with exp. intro x ; rewrite <- (derive_pt_exp x) ; apply pr_nu_var ; reflexivity. apply IHn. Qed.
imports: Reals Rsequence_def Rfunction_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def Rfunction_classes_facts Rextensionality Rpser_def Rpser_def Rpser_cv_facts Rpser_sums Rpser_sums_facts Rpser_derivative