proposition: Lemma D_scal : forall n f a, D n f -> D n (mult_real_fct a f).
proof: Proof. intro n ; induction n ; intros f a Dnf ; inversion_clear Dnf. constructor. apply D_S with (derivable_scal _ _ pr) ; apply D_ext with (mult_real_fct a (derive f pr)). unfold mult_real_fct ; intro x ; symmetry ; unfold derive ; rewrite derive_pt_eq ; apply derivable_pt_lim_scal ; eapply derive_pt_eq_1 ; auto. apply IHn ; assumption. Qed.
imports: Rbase Ranalysis Lia Lra Rfunctions Rfunction_facts Rextensionality Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def MyR_dist Reals.Tactics