proposition: Lemma limit_div_neg_imp : forall (f : R -> R) (D D1 : R -> Prop) (l : R), (forall x0 : R, D1 x0 -> D x0) -> limit_div_neg f D l -> limit_div_neg f D1 l.
proof: Proof. intros. intros m Hm. specialize (H0 m Hm). destruct H0 as [alp [Halp Hsolve]]. exists alp. split. apply Halp. intros. assert (D x). intuition. specialize (Hsolve x H2 H1). apply Hsolve. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality