proposition: Lemma derivable_Rball_derivable_pt: forall f c r, derivable_Rball c r f -> forall x, Rball c r x -> derivable_pt f x.
proof: Proof. intros f lb ub H x Dx ; destruct (H x Dx) as [l Hl] ; exists l ; eapply derivable_pt_lim_Rball_pt_lim ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics