proposition: Theorem Hopital_gpinf_Lfin_right : limit1_in (fun x => f x / g x) (open_interval a b) L a.
proof: Proof. destruct g_not_zero as [a' [H1 Ha']]. unfold limit1_in, limit_in. intros. assert (Hacc2' : forall x y, open_interval a a' x -> open_interval a a' y -> x < y -> exists c, exists Hopenc, f x / g x = (1 - (g y / g x)) * derive_pt f c (Df c Hopenc) / derive_pt g c (Dg c Hopenc) + (f y / g x) /\ x < c < y). intros. assert (open_interval a b x). split. now apply H0. apply Rlt_trans with a'. now apply H0. now apply H1. assert (open_interval a b y). split. now apply H2. apply Rlt_trans with a'. now apply H2. now apply H1. generalize (MVT_unusable a' H1 x y H0 H2 H3). intros Hacc2'. destruct Hacc2' as [c [Hopenc [Hacc2' H7]]]. exists c. exists Hopenc. split; [ | now intuition]. apply (Rplus_eq_reg_l (- (f y / g x))). ring_simplify. apply (Rmult_eq_reg_l (g x)). apply (Rmult_eq_reg_l (derive_pt g c (Dg c Hopenc))). apply (Rmult_eq_reg_l (-1)). field_simplify. field_simplify in Hacc2'. replace (derive_pt g c (Dg c Hopenc) * f y - derive_pt g c (Dg c Hopenc) * f x) with (f y * derive_pt g c (Dg c Hopenc) - f x * derive_pt g c (Dg c Hopenc)) by ring. rewrite Hacc2'. now field. split. apply Ha'. now apply H0. now apply (g'_not_0 c Hopenc). now apply Ha'; assumption. intro. now lra. now apply g'_not_0. now apply Ha'; assumption. assert (H0: forall eps, eps > 0 -> exists y, open_interval a a' y /\ forall c (Hopen : open_interval a y c) (Hopenc : open_interval a b c), R_dist (derive_pt f c (Df c Hopenc) / derive_pt g c (Dg c Hopenc)) L < eps). intros eps0 Heps0. specialize (Hlimder eps0 Heps0). destruct Hlimder as [alp [Halp Hlimder1]]. exists (a + Rmin ((a'-a) / 2) alp). split. apply open_lemma. now apply H1. now apply Halp. intros. specialize (Hlimder1 c Hopenc). unfold R_dist in *. apply Hlimder1. destruct Hopen. apply Rlt_le_trans with (Rmin ((a' - a) / 2) alp). now rewrite Rabs_right; lra. now apply Rmin_r. assert (H15 : forall A eps, eps > 0 -> exists alp, alp > 0 /\ forall x, open_interval a b x -> R_dist x a < alp -> Rabs (A / g x) < eps). intros. unfold limit_div_pos in Zg. destruct (Req_dec A 0) as [eq_dec1 | eq_dec2]. subst. exists 1. intuition. unfold Rdiv. rewrite Rmult_0_l. rewrite Rabs_R0. now assumption. specialize (Zg (Rabs A / eps0)). assert (Rabs A /eps0 > 0). assert (Rabs A > 0). apply Rabs_pos_lt. now assumption. unfold Rdiv. assert (/eps0 > 0). now apply Rinv_0_lt_compat; assumption. now apply Rmult_lt_0_compat; assumption. specialize (Zg H3). destruct Zg as [alp [Halp Zg3]]. exists alp. intuition. unfold Rdiv. rewrite Rabs_mult. specialize (Zg3 x H4 H5). assert (g x > 0). apply Rlt_trans with (Rabs A / eps0). now assumption. now assumption. rewrite Rabs_Rinv. rewrite (Rabs_right (g x)). apply (Rmult_lt_reg_l (g x)). now assumption. apply (Rmult_lt_reg_l (/eps0)). apply Rinv_0_lt_compat. now apply H2. field_simplify. unfold Rdiv. try rewrite Rinv_1. try rewrite Rmult_1_r. now apply Zg3. intro. now lra. split. intro. now lra. intro. now lra. now lra. intro. now lra. assert (Heps4 : eps / 4 > 0) by lra. assert (bizarre : forall eps L, L >= 0 -> eps > 0 -> exists eps1, eps1 > 0 /\ eps1 * (L + eps) < eps / 2). intros. exists (/2 * ((eps0 / 2) * / (L0 + eps0))). split. apply Rmult_lt_0_compat. now lra. apply Rmult_lt_0_compat. now lra. apply Rinv_0_lt_compat. now lra. field_simplify. now lra. intro. now lra. specialize (H0 (eps/4) Heps4). destruct H0 as [y [open H0]]. specialize (Hlimder eps H). destruct Hlimder as [alp1 [Halp1 Hlim2]]. generalize (H15 (f y) (eps/4) Heps4). intros H16. destruct H16 as [alp2 [Halp2 Hlim3]]. specialize (bizarre eps (Rabs L)). assert (Hb1: Rabs L >= 0) by (apply Rle_ge; apply Rabs_pos). specialize (bizarre Hb1 H). destruct bizarre as [eps1 [Heps1 HepsL4]]. specialize (H15 (g y) eps1 Heps1). destruct H15 as [alp3 [Halp3 Hlim4]]. pose (alp_alp := Rmin (Rmin alp1 alp2) alp3). pose (alp := Rmin (Rmin alp_alp (a' - a)) (y - a)). exists alp. split. apply Rmin_pos. apply Rmin_pos. apply Rmin_pos. now apply Rmin_pos; assumption. now assumption. unfold open_interval in H1. destruct H1. now lra. unfold open_interval in open. destruct open. now lra. intros. specialize (Hacc2' x y). assert (open_interval a a' x). unfold dist in H2. simpl in H2. unfold R_dist in H2. split. now apply H2. assert (Rabs (x - a) < Rabs (a' - a)). rewrite (Rabs_right (a' - a)). unfold alp in H2. apply Rlt_le_trans with (Rmin (Rmin alp_alp (a' - a)) (y - a)). now intuition. apply Rle_trans with (Rmin alp_alp (a' - a)). now apply Rmin_l. now apply Rmin_r. destruct H1. now lra. do 2 rewrite Rabs_right in H3. now lra. now destruct H1; lra. destruct H2. now destruct H2; lra. destruct H2. now destruct H2; lra. assert (open_interval a a' y). now apply open. specialize (Hacc2' H3 H4). assert (x < y). unfold alp in H2. unfold dist in H2. simpl in H2. unfold R_dist in H2. assert (Rabs (x - a) < Rabs (y - a)). rewrite (Rabs_right (y - a)). unfold alp in H2. apply Rlt_le_trans with (Rmin (Rmin alp_alp (a' - a)) (y - a)). now intuition. now apply Rmin_r. destruct H4. now lra. do 2 rewrite Rabs_right in H5. now lra. now destruct H4; lra. now destruct H3; lra. now destruct H3; lra. specialize (Hacc2' H5). destruct Hacc2' as [c [Hopenc H10]]. destruct H10 as [H10 H100]. rewrite H10. unfold dist. simpl. unfold R_dist. unfold Rdiv. ring_simplify (((1 - g y */ g x) * derive_pt f c (Df c Hopenc) */ derive_pt g c (Dg c Hopenc) + f y */ g x - L)). unfold Rminus. rewrite Rplus_assoc. rewrite Rplus_assoc. apply Rle_lt_trans with (Rabs (- g y * / g x * derive_pt f c (Df c Hopenc) * / derive_pt g c (Dg c Hopenc)) + Rabs (/ g x * f y + ( derive_pt f c (Df c Hopenc) * / derive_pt g c (Dg c Hopenc) +- L))). now apply Rabs_triang. replace (- g y * / g x * derive_pt f c (Df c Hopenc) */ derive_pt g c (Dg c Hopenc)) with ((- g y * / g x) * (derive_pt f c (Df c Hopenc) */ derive_pt g c (Dg c Hopenc))) by ring. rewrite Rabs_mult. replace eps with (eps / 2 + eps / 2) by field. apply Rplus_lt_compat. apply Rle_lt_trans with (eps1 * (Rabs L + eps)). apply Rmult_le_compat. now apply Rabs_pos. now apply Rabs_pos. rewrite Ropp_mult_distr_l_reverse. rewrite Rabs_Ropp. apply Rlt_le. apply Hlim4. now apply H2. unfold alp in H2. unfold alp_alp in H2. apply Rlt_le_trans with ((Rmin (Rmin alp1 alp2) alp3)). apply Rlt_le_trans with (Rmin (Rmin (Rmin alp1 alp2) alp3) (a' - a)). apply Rlt_le_trans with (Rmin (Rmin (Rmin (Rmin alp1 alp2) alp3) (a' - a)) (y - a)). now apply H2. now apply Rmin_l. now apply Rmin_l. now apply Rmin_r. destruct H2. assert (R_dist x a < alp1). unfold alp in H6. unfold alp_alp in H6. apply Rlt_le_trans with (Rmin alp1 alp2). apply Rlt_le_trans with (Rmin (Rmin alp1 alp2) alp3). apply Rlt_le_trans with (Rmin (Rmin (Rmin alp1 alp2) alp3) (a' - a)). apply Rlt_le_trans with (Rmin (Rmin (Rmin (Rmin alp1 alp2) alp3) (a' - a)) (y - a)). now apply H6. now apply Rmin_l. now apply Rmin_l. now apply Rmin_l. now apply Rmin_l. assert (open_interval a y c). unfold open_interval. split. apply Rlt_trans with x. now apply H2. now apply H100. now apply H100. specialize (H0 c H8). specialize (H0 Hopenc). assert (Rabs (derive_pt f c (Df c Hopenc) / derive_pt g c (Dg c Hopenc)) - Rabs L <= eps). apply Rle_trans with (R_dist (derive_pt f c (Df c Hopenc) / derive_pt g c (Dg c Hopenc)) L). apply Rle_trans with (Rabs (Rabs (derive_pt f c (Df c Hopenc) / derive_pt g c (Dg c Hopenc)) - Rabs L)). now apply Rle_abs. unfold R_dist. now apply Rabs_triang_inv2. apply Rlt_le. apply Rlt_trans with (eps / 4). now apply H0. now lra. apply (Rplus_le_reg_l (- Rabs L)). ring_simplify. rewrite Rplus_comm. now apply H9. now apply HepsL4. replace (eps /2) with (eps / 4 + eps / 4) by field. apply Rle_lt_trans with (Rabs (/ g x * f y) + Rabs (derive_pt f c (Df c Hopenc) * / derive_pt g c (Dg c Hopenc) + - L)). now apply Rabs_triang. apply Rplus_lt_compat. rewrite Rmult_comm. apply Hlim3. now apply H2. destruct H2. unfold alp in H6. unfold alp_alp in H6. apply Rlt_le_trans with (Rmin alp1 alp2). apply Rlt_le_trans with ((Rmin (Rmin alp1 alp2) alp3)). apply Rlt_le_trans with (Rmin (Rmin (Rmin alp1 alp2) alp3) (a' - a)). apply Rlt_le_trans with (Rmin (Rmin (Rmin (Rmin alp1 alp2) alp3) (a' - a)) (y - a)). now apply H6. now apply Rmin_l. now apply Rmin_l. now apply Rmin_l. now apply Rmin_r. apply H0. unfold R_dist in Hlim2. unfold open_interval in *. split. now apply Hopenc. apply H100. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality