proposition: Lemma derive_pt_Rball_scal: forall a f c r x pr pr', Rball c r x -> derive_pt_in (Rball c r) (mult_real_fct a f) x pr = a * derive_pt_in (Rball c r) f x pr'.
proof: Proof. intros a f c r x [] [] x_in ; eapply derivable_pt_lim_in_derive_pt_Rball, derivable_pt_lim_in_scal ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics