proposition: Lemma limit1_in_open : forall f L a b c, open_interval a b c -> limit1_in f (open_interval a c) L a -> limit1_in f (open_interval a b) L a.
proof: Proof. intros. unfold limit1_in in *. unfold limit_in in *. intros. specialize (H0 eps H1). destruct H0 as [alp [Halp Hlim]]. exists (Rmin alp (c - a)). split. apply Rmin_glb_lt. now assumption. now destruct H; lra. intros. apply Hlim. destruct H0. unfold dist in *. simpl in *. unfold R_dist in *. split. split. now destruct H0; assumption. assert (Rabs (x - a) < c - a). apply Rlt_le_trans with (Rmin alp (c - a)). now apply H2. now apply Rmin_r. now rewrite Rabs_right in H3; destruct H0; lra. apply Rlt_le_trans with (Rmin alp (c - a)). now apply H2. apply Rmin_l. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality