proposition: Lemma Hopital_gninf_Lfin_right : forall (f g : R -> R) (a b L : R), a < b -> forall (Df : forall x : R, open_interval a b x -> derivable_pt f x) (Dg : forall x : R, open_interval a b x -> derivable_pt g x), (forall x : R, a <= x <= b -> continuity_pt f x) -> (forall x : R, a <= x <= b -> continuity_pt g x) -> limit_div_neg g (open_interval a b) a -> (forall (x : R) (Hopen : open_interval a b x), derive_pt g x (Dg x Hopen) <> 0) -> (forall eps : R, eps > 0 -> exists alp : R, alp > 0 /\ (forall (x : R) (Hopen : open_interval a b x), R_dist x a < alp -> R_dist (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)) L < eps)) -> limit1_in (fun x : R => f x / g x) (open_interval a b) L a.
proof: Proof. intros. destruct (g_not_zero2 g a b H H2) as [a' [Hopen Ha']]. apply limit1_in_open with a'. now apply Hopen. apply limit1_ext with (fun x => - ( f x / (- g x))). intros. field. apply Ha'. now apply H5. replace L with (- - L) by ring. apply limit_Ropp. assert (Dg' : forall x : R, open_interval a a' x -> derivable_pt (- g) x). intros. reg. apply Dg. split. now apply H5. apply Rlt_trans with a'. now apply H5. now apply Hopen. assert (Df' : forall x : R, open_interval a a' x -> derivable_pt f x). intros. apply Df. split. now apply H5. apply Rlt_trans with a'. now apply H5. now apply Hopen. apply Hopital_gpinf_Lfin_right with Df' Dg'. now apply Hopen. intros. apply H0. split. now apply H5. apply Rle_trans with a'. now apply H5. apply Rlt_le. now apply Hopen. intros. reg. apply H1. split. now apply H5. apply Rle_trans with a'. now apply H5. apply Rlt_le. now apply Hopen. apply limit_div_Ropp. now apply Hopen. apply limit_div_neg_open1 with b. now assumption. now apply H2. intros. assert (Dg'' : forall x, open_interval a a' x -> derivable_pt g x). intros. apply Dg. split. now apply H5. apply Rlt_trans with a'. now apply H5. now apply Hopen. rewrite (pr_nu (-g)%F x _ (derivable_pt_opp g x (Dg'' x Hopen0))). rewrite derive_pt_opp. apply Ropp_neq_0_compat. assert (Hder : open_interval a b x). unfold open_interval in *. split. now apply Hopen0. now destruct Hopen, Hopen0; lra. rewrite (pr_nu g x _ (Dg x Hder)). now apply H3. intros. specialize (H4 eps H5). destruct H4 as [alp [Halp H10]]. exists alp. split. now assumption. intros. assert (Hder : open_interval a b x). unfold open_interval in *. split. now apply Hopen0. now destruct Hopen, Hopen0; lra. specialize (H10 x Hder H4). unfold R_dist in *. replace (derive_pt (- g) x (Dg' x Hopen0)) with (- derive_pt g x (Dg x Hder)). replace (derive_pt f x (Df' x Hopen0)) with (derive_pt f x (Df x Hder)). replace (derive_pt f x (Df x Hder) / - derive_pt g x (Dg x Hder) - - L) with (- (derive_pt f x (Df x Hder) / derive_pt g x (Dg x Hder) - L)). rewrite Rabs_Ropp. now assumption. field. now apply H3. now apply pr_nu. assert (Dg'' : forall x, open_interval a a' x -> derivable_pt g x). intros. apply Dg. split. now apply H6. apply Rlt_trans with a'. now apply H6. now apply Hopen. rewrite (pr_nu (-g)%F x _ (derivable_pt_opp g x (Dg'' x Hopen0))). rewrite derive_pt_opp. apply Ropp_eq_compat. apply pr_nu. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality