proposition: Lemma derivable_pt_lim_derive_pt_open_interval: forall f lb ub x l (pr : derivable_pt_in (open_interval lb ub) f x), open_interval lb ub x -> derivable_pt_lim_in (open_interval lb ub) f x l -> derive_pt_in (open_interval lb ub) f x pr = l.
proof: Proof. intros f lb ub x l [l' Hl'] x_in Hl ; eapply derivable_pt_lim_open_interval_uniqueness ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics