proposition: Lemma derive_open_interval_derive : forall f lb ub x pr pr', open_interval lb ub x -> derive_open_interval lb ub f pr x = derive f pr' x.
proof: Proof. intros f lb ub x pr pr' x_in ; unfold derive_open_interval, derive. destruct (in_open_interval_dec lb ub x). apply derive_open_interval_pt ; assumption. contradiction. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics