proposition: Lemma Hopital_g0_Lninf_right : forall m, m < 0 -> exists alp, alp > 0 /\ (forall x (Hopen: open_interval a b x), R_dist x a < alp -> m > (f x) / (g x)).
proof: Proof. intros m Hm. specialize (Hlimder m Hm). destruct Hlimder as [alp [Halp Hlim]]. exists alp. split. now assumption. intros. assert (Hacc2 : forall x, open_interval a b x -> exists c, exists Hopenc, f x / g x = derive_pt f c (Df c Hopenc) / derive_pt g c (Dg c Hopenc) /\ a < c < x). generalize MVT. intros. specialize (H0 f g a x0). assert (forall c, a < c < x0 -> derivable_pt f c). intros. apply Df. unfold open_interval. split. now intuition. now apply Rlt_trans with x0; unfold open_interval in H1; intuition. assert (forall c, a < c < x0 -> derivable_pt g c). intros. apply Dg. unfold open_interval. split. now intuition. now apply Rlt_trans with x0; unfold open_interval in H1; intuition. specialize (H0 H2 H3). assert (a < x0) by (unfold open_interval in H1; intuition). assert (forall c : R, a <= c <= x0 -> continuity_pt f c). intros. apply Cf. split. now intuition. unfold open_interval in H1. now apply Rle_trans with x0; intuition. assert (forall c, a <= c <= x0 -> continuity_pt g c). intros. apply Cg. split. now intuition. unfold open_interval in H1. now apply Rle_trans with x0; intuition. specialize (H0 H4 H5 H6). destruct H0 as [c [P Hold2]]. exists c. assert (Hopenc : open_interval a b c). unfold open_interval in *. split. now apply P. apply Rlt_trans with x0. now apply P. now apply H1. exists Hopenc. split. rewrite (g_a_zero g a b) in Hold2. rewrite (f_a_zero f a b) in Hold2. do 2 rewrite Rminus_0_r in Hold2. apply (Rmult_eq_reg_l (g x0)). rewrite (pr_nu f c _ (H2 c P)). unfold Rdiv. do 2 rewrite <- Rmult_assoc. rewrite Hold2. rewrite (pr_nu g c _ (Dg c Hopenc)). field. generalize (g_not_0 c Hopenc). generalize (g_not_0 x0 H1). intros H01 H02. assert (c < b). now unfold open_interval in Hopenc; destruct Hopenc; assumption. split. now apply H02. now apply H01. apply g_not_0. now apply H1. apply Hab. apply Cf. apply Zf. apply Hab. apply Cg. apply Zg. now apply P. specialize (Hacc2 x Hopen). destruct Hacc2 as [c [Hopenc Haccc]]. specialize (Hlim c Hopenc). unfold R_dist in *. assert (open_interval a b c /\ Rabs (c - a) < alp). split. now apply Hopenc. destruct Haccc. destruct H1. rewrite Rabs_right. rewrite Rabs_right in H. now lra. now lra. now lra. destruct H0. specialize (Hlim H1). destruct Haccc. rewrite H2. apply Hlim. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality