proposition: Lemma derivable_pt_lim_open_interval_uniqueness: forall f lb ub x l l', open_interval lb ub x -> derivable_pt_lim_in (open_interval lb ub) f x l -> derivable_pt_lim_in (open_interval lb ub) f x l' -> l = l'.
proof: Proof. intros ; eapply derivable_pt_lim_in_uniqueness ; try eassumption. apply dense_open_interval. eapply open_interval_inhabited ; eassumption. eapply open_interval_interval ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics