proposition: Lemma derivable_pt_lim_scal : forall f a x l, derivable_pt_lim f x l -> derivable_pt_lim (fun x => a * f x) x (a * l).
proof: Proof. intros. assert (H0 := derivable_pt_lim_const a x). replace (mult_real_fct a f) with (fct_cte a * f)%F. replace (a * l) with (C0 * f x + a * l); [ idtac | ring ]. apply (derivable_pt_lim_mult (fct_cte a) f x 0 l); assumption. unfold mult_real_fct, mult_fct, fct_cte in |- *; reflexivity. 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