proposition: Lemma limit_open : forall f a b, limit1_in f (D_x no_cond a) (f a) a -> limit1_in f (open_interval a b) (f a) a.
proof: Proof. clear Hlimder Zf Zg. unfold limit1_in in *. unfold limit_in in *. intros. specialize (H eps H0). destruct H as [alp [Halp H2]]. exists alp. split. now apply Halp. intros. apply H2. destruct H. split. constructor. now constructor. unfold open_interval in H. now intro; destruct H; lra. apply H1. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality