proposition: Theorem Hopital_gninf_Lninf_right : limit_div_neg (fun x => f x / g x) (open_interval a b) a.
proof: Proof. apply limit_div_neg_inv. apply limit_div_pos_ext with (fun x => (- f x) / g x). intros. unfold Rdiv. ring. assert (Df' : forall x : R, open_interval a b x -> derivable_pt (-f) x). intros. reg. apply Df. apply H. apply Hopital_gninf_Lpinf_right with Df' Dg; try assumption. intros. reg. apply Cf. apply H. intros m Hm. assert (Hm' : - m < 0) by lra. destruct (Hlimder (-m) Hm') as [alp [Halp Hsolve]]. exists alp. split. assumption. intros. specialize (Hsolve x Hopen H). rewrite (pr_nu _ _ _ (derivable_pt_opp f x (Df x Hopen))). rewrite derive_pt_opp. replace m with (--m) by ring. unfold Rdiv. rewrite Ropp_mult_distr_l_reverse. apply Ropp_gt_lt_contravar. apply Hsolve. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality