proposition: Lemma derivable_pt_lim_open_interval_pt_lim : forall lb ub f x l, open_interval lb ub x -> derivable_pt_lim_in (open_interval lb ub) f x l -> derivable_pt_lim f x l.
proof: Proof. intros lb ub f x l x_in Hl eps eps_pos ; destruct (Hl _ eps_pos) as [d [d_pos Hd]] ; simpl in Hd ; unfold R_dist in Hd. pose (delta := Rmin (interval_dist lb ub x) d). assert (delta_pos : 0 < delta). apply Rmin_pos_lt ; [apply open_interval_dist_pos |] ; assumption. exists (mkposreal _ delta_pos) ; intros h h_neq h_bd ; specialize (Hd (x + h)) ; unfold growth_rate in * ; replace (x + h - x) with h in Hd by ring ; apply Hd ; split. split. apply open_interval_dist_bound ; [apply open_interval_interval | eapply Rlt_le_trans ; [| eapply Rmin_l]] ; eassumption. clear -h_neq ; intro Hf ; apply h_neq, Rplus_eq_reg_l with x ; rewrite <- Hf ; ring. eapply Rlt_le_trans ; [eassumption | eapply Rmin_r]. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics