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