proposition: Theorem Hopital_gpinf_Lpinf_left : limit_div_pos (fun x => f x / g x) (open_interval a b) b.
proof: Proof. apply limit_div_pos_ext with (comp (fun x => f (- x) / g (- x)) (fun x => -x)). intros. unfold comp. ring_simplify (--x). reflexivity. apply limit_div_pos_comp_Ropp. assert (Df': forall x, open_interval (-b) (-a) x -> derivable_pt (fun x => f (- x)) x). intros. reg. apply Df. now destruct H; split; lra. assert (Dg': forall x, open_interval (-b) (-a) x -> derivable_pt (fun x => g (- x)) x). intros. reg. apply Dg. now destruct H; split; lra. intros m Hm. apply Hopital_gpinf_Lpinf_right with Df' Dg'. now intuition. intros. reg. apply Cf. now destruct H; split; lra. intros. reg. apply Cg. now destruct H; split; lra. apply limit_div_pos_ext with (comp g (fun x => -x)). intros. reflexivity. apply limit_div_pos_comp_Ropp_l. do 2 rewrite Ropp_involutive. apply Zg. intros. assert (Hopen' : open_interval a b (-x)). destruct Hopen; split; lra. rewrite <- (derive_pt_comp_Ropp _ _ _ _ Dg _ _ Hopen'). replace 0 with (-0) by ring. intro. apply Ropp_eq_compat in H. do 2 rewrite Ropp_involutive in H. apply g'_not_0 in H. apply H. intros m1 Hm1. specialize (Hlimder m1 Hm1). destruct Hlimder as [alp [Halp Hsolve1]]. exists alp. split. apply Halp. intros. assert (Hopenx : open_interval a b (-x)). destruct Hopen; split; lra. replace (derive_pt (fun x0 : R => f (- x0)) x (Df' x Hopen)) with (- derive_pt f (- x) (Df (- x) Hopenx)). replace (derive_pt (fun x0 : R => g (- x0)) x (Dg' x Hopen)) with (- derive_pt g (- x) (Dg (- x) Hopenx)). replace ((- derive_pt f (- x) (Df (- x) Hopenx) / - derive_pt g (- x) (Dg (- x) Hopenx))) with ((derive_pt f (- x) (Df (- x) Hopenx) / derive_pt g (- x) (Dg (- x) Hopenx))). apply Hsolve1. unfold R_dist in *. replace (- x - b) with (- (x + b)) by ring. ring_simplify (x -- b) in H. rewrite Rabs_Ropp. apply H. field. apply g'_not_0. apply derive_pt_comp_Ropp. apply derive_pt_comp_Ropp. lra. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality