proposition: Lemma derive_pt_scal : forall f (a x:R) (pr:derivable_pt f x), derive_pt (mult_real_fct a f) x (derivable_pt_scal _ _ _ pr) = a * derive_pt f x pr.
proof: Proof. intros. assert (H := derivable_derive f x pr). assert (H0 := derivable_derive (mult_real_fct a f) x (derivable_pt_scal _ _ _ pr)). elim H; clear H; intros l1 H. elim H0; clear H0; intros l2 H0. rewrite H; apply derive_pt_eq_0. assert (H3 := proj2_sig pr). unfold derive_pt in H; rewrite H in H3. apply derivable_pt_lim_scal; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv