proposition: Lemma limit_div_neg_open1 : forall f a b c, open_interval a b c -> limit_div_neg f (open_interval a b) a -> limit_div_neg f (open_interval a c) a.
proof: Proof. intros. unfold limit_div_neg in *. intros. specialize (H0 m H1). destruct H0 as [alp [Halp Hlim]]. exists alp. intuition. apply Hlim. now destruct H; destruct H0; split; lra. apply H2. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality