proposition: Lemma derivable_pt_lim_interval_uniqueness: forall (f : R -> R) (lb ub x l l' : R), lb < ub -> interval lb ub x -> derivable_pt_lim_in (interval lb ub) f x l -> derivable_pt_lim_in (interval lb ub) f x l' -> l = l'.
proof: Proof. intros ; eapply derivable_pt_lim_in_uniqueness ; try eassumption. apply dense_interval ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics