proposition: Lemma derivable_pt_lim_in_derive_Rball: forall c r f x l pr, Rball c r x -> derivable_pt_lim_in (Rball c r) f x l -> derive_Rball c r f pr x = l.
proof: Proof. intros c r f x l pr x_in Hl ; unfold derive_Rball ; destruct (in_Rball_dec c r x) as [x_in2 | x_nin]. eapply derivable_pt_lim_in_derive_pt_Rball ; eassumption. contradiction. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics