proposition: Lemma derivable_open_interval_derivable : forall f, (forall lb ub, derivable_open_interval lb ub f) -> derivable f.
proof: Proof. intros f Hf x ; eapply derivable_open_interval_pt, (center_in_open_interval _ 1). apply Hf. lra. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics