proposition: Lemma derivable_pt_lim_in_uniqueness: forall (D : R -> Prop) f x l l', dense D x -> derivable_pt_lim_in D f x l -> derivable_pt_lim_in D f x l' -> l = l'.
proof: Proof. intros D f x l l' Dx Hl ; eapply single_limit ; try eassumption ; intros eps eps_pos ; destruct (Dx _ eps_pos) as [y [y_h y_bd]] ; exists y. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics