proposition: Lemma derive_pt_in_open_interval_uniqueness : forall f x lb ub pr pr', open_interval lb ub x -> derive_pt_in (open_interval lb ub) f x pr = derive_pt_in (open_interval lb ub) f x pr'.
proof: Proof. intros f x lb ub [] [] x_in ; 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