proposition: Lemma derivable_pt_lim_Rball_uniqueness: forall c r f x l l', Rball c r x -> derivable_pt_lim_in (Rball c r) f x l -> derivable_pt_lim_in (Rball c r) f x l' -> l = l'.
proof: Proof. intros ; eapply derivable_pt_lim_in_uniqueness ; try eassumption ; apply dense_Rball ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics