proposition: Lemma derive_Rball_scal: forall a f c r x pr pr', derive_Rball c r (mult_real_fct a f) pr x = a * derive_Rball c r f pr' x.
proof: Proof. intros ; unfold derive_Rball ; destruct (in_Rball_dec c r x) as [x_in | x_nin] ; [apply derive_pt_Rball_scal ; assumption | symmetry ; apply Rmult_0_r]. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics