proposition: Lemma derivable_pt_lim_scal : forall f (a x l:R), derivable_pt_lim f x l -> derivable_pt_lim (mult_real_fct a f) 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 (0 * 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; reflexivity. Qed.
imports: Rbase Rfunctions Rlimit Rderiv