proposition: Lemma C_infty_const : forall (c : R), C_infty (fct_cte c).
proof: Proof. intros c n ; destruct n. constructor ; reg. apply C_S with (derivable_const c) ; apply C_ext with (fct_cte 0). intro x ; unfold derive ; symmetry ; rewrite derive_pt_eq ; apply derivable_pt_lim_const. apply C_infty_zero. 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