proposition: Lemma limit_div_Ropp : forall a b g, a < b -> limit_div_neg g (open_interval a b) a -> limit_div_pos (fun x : R => - g x) (open_interval a b) a.
proof: Proof. intros. unfold limit_div_pos, limit_div_neg in *. intros. specialize (H0 m H1). destruct H0. exists x. split. now intuition. intros. destruct H0. specialize (H4 x0 H2 H3). lra. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality