proposition: Lemma derivable_pt_scal : forall f (a x:C), derivable_pt f x -> derivable_pt (mult_real_fct a f) x.
proof: Proof. unfold derivable_pt in |- *; intros f1 a x X. elim X; intros. exists (a * x0). apply derivable_pt_lim_scal; assumption. Qed.
imports: MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Ranalysis_MVT Canalysis_diff Cprop_base Cnorm Ctacfield Cmet Canalysis_def Cderiv