proposition: Lemma C_infty_monomial : forall d a, C_infty (fun x => Rmult a (pow x d)).
proof: Proof. intro d ; induction d ; intros a n. apply C_ext with (fct_cte a). intro ; ring_simplify ; reflexivity. eapply C_infty_const. destruct n. constructor; intro; reg. assert (pr : derivable (fun x : R => (a * x ^ S d)%R)) by reg ; apply C_S with pr ; apply C_ext with (fun x => (a * INR (S d) * pow x d)%R). intro x ; symmetry ; pose (fmod := mult_real_fct a (fun x0 : R => (x0 ^ S d)%R)) ; transitivity (derive_pt _ x (derivable_pt_scal _ a x (derivable_pt_pow (S d) _))). apply pr_nu. rewrite derive_pt_scal, Rmult_assoc ; apply Rmult_eq_compat_l ; apply derive_pt_pow. eapply IHd. 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