proposition: Lemma limit_div_neg_comp_Ropp_l : forall (g : R -> R) (a b : R), limit_div_neg g (open_interval (-a) (-b)) (-b) -> limit_div_neg (comp g (fun x => -x)) (open_interval b a) b.
proof: Proof. intros. intros m Hm. specialize (H m Hm). destruct H as [alp [Halp Hsolve]]. exists alp. split. apply Halp. intros. specialize (Hsolve (-x)). apply Hsolve. split; destruct H; lra. unfold R_dist in *. replace (- x - - b) with (- (x - b)) by ring. rewrite Rabs_Ropp. apply H0. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality