proposition: Lemma extend_continuously_derivable_open_interval : forall a b f, Ranalysis_def.derivable_open_interval a b f -> Ranalysis_def.derivable_open_interval a b (extend_continuously f a b).
proof: Proof. intros a b f f_deriv x x_in ; eapply derivable_pt_in_ext_strong, f_deriv ; try assumption. apply extend_continuously_extends_open_interval. Qed.
imports: Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Rbase MyRIneq MyR_dist Rfunctions Lra