proposition: Lemma differentiable_pt_lim_scal : forall f a x v l, v <> C0 -> differentiable_pt_lim f x v l -> differentiable_pt_lim (fun x => a * f x) x v (a * l).
proof: Proof. intros f a x v l v_neq f_diff. assert (H0 := differentiable_pt_lim_const a x v). replace (mult_real_fct a f) with (fct_cte a * f)%F. replace (a * l) with (C0 * f x + a * l); [ idtac | ring ]. apply (differentiable_pt_lim_mult (fct_cte a) f x v 0 l) ; assumption. unfold mult_real_fct, mult_fct, fct_cte in |- *; reflexivity. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def