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