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