proposition: Theorem Hopital_gninf_Lpinf_right : limit_div_pos (fun x => f x / g x) (open_interval a b) a.
proof: Proof. destruct new_bound as (b', H0). apply limit_div_pos_open with b'. intuition. assert (Df' : forall x, open_interval a b' x -> derivable_pt f x). intros. apply Df. destruct H; split; destruct H0 as [H5 [H2 H4]]; lra. assert (Dg' : forall x, open_interval a b' x -> derivable_pt g x). intros. apply Dg. destruct H; split; destruct H0 as [H5 [H2 H4]]; lra. destruct H0. destruct H0. apply Hopital_infinite_inf_neg_lpos_useless with Df' Dg'. apply H0. intros. apply Cf. intuition. lra. intros. apply Cg; intuition; lra. apply (limit_div_neg_open1 g a b b'). split; assumption. apply Zg. intros. assert (Hopen2 : open_interval a b x). destruct Hopen; split. apply H2. lra. rewrite (pr_nu _ _ _ (Dg x Hopen2)). apply g'_not_0. intros m Hm. specialize (Hlimder m Hm). destruct Hlimder as [alp [Halp Hsolve]]. exists alp. split. assumption. intros. assert (Hopen2 : open_interval a b x). split; destruct Hopen; lra. specialize (Hsolve x Hopen2 H2). replace (derive_pt f x (Df' x Hopen)) with (derive_pt f x (Df x Hopen2)) by (apply pr_nu). replace (derive_pt g x (Dg' x Hopen)) with (derive_pt g x (Dg x Hopen2)) by (apply pr_nu). apply Hsolve. intuition. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality