proposition: Lemma derivable_pt_lim_Rball_pt_lim: forall f c r x l, Rball c r x -> derivable_pt_lim_in (Rball c r) f x l -> derivable_pt_lim f x l.
proof: Proof. intros ; eapply derivable_pt_lim_open_interval_pt_lim. eapply included_Rball_open_interval ; eassumption. eapply derivable_pt_lim_in_contravariant. eapply included_open_interval_Rball2 ; eassumption. eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics