proposition: Lemma limit_div_neg_inv : forall f a b, limit_div_pos (fun x => - f x) (open_interval a b) a -> limit_div_neg f (open_interval a b) a.
proof: Proof. intros. unfold limit_div_pos, limit_div_neg in *. intros m Hm. specialize (H m Hm). destruct H as [alp [Halp Hsolve]]. exists alp. split. assumption. intros. specialize (Hsolve x H H0). lra. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality