proposition: Lemma derive_open_interval_unfold : forall a b f f_deriv c (c_in : open_interval a b c), derive_open_interval a b f f_deriv c = derive_pt_in (open_interval a b) f c (f_deriv c c_in).
proof: Proof. intros a b f f_deriv c c_in ; unfold derive_open_interval ; destruct (in_open_interval_dec a b c) as [c_in' | hf]. + apply derive_pt_in_open_interval_uniqueness ; assumption. + contradiction. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics