proposition: Lemma extend_continuously_derive_open_interval : forall a b f fext_deriv f_deriv c, (derive_open_interval a b (extend_continuously f a b) fext_deriv c = derive_open_interval a b f f_deriv c)%R.
proof: Proof. intros a b f fext_deriv f_deriv c ; unfold derive_open_interval ; destruct (in_open_interval_dec a b c) as [c_in | c_out]. + apply derive_pt_in_ext_strong. - apply dense_open_interval. * transitivity c ; apply c_in. * apply open_interval_interval ; assumption. - assumption. - intros ; symmetry ; eapply extend_continuously_extends_open_interval ; assumption. + reflexivity. Qed.
imports: Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Rbase MyRIneq MyR_dist Rfunctions Lra