proposition: Theorem Hopital_gpinf_Lninf_right : limit_div_neg (fun x => f x / g x) (open_interval a b) a.
proof: Proof. destruct (g_not_zero g a b Hab Zg) as [a' [H1 Ha']]. unfold limit_div_neg. intros eps H. 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 f g a b Df Dg Cf Cg 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), (derive_pt f c (Df c Hopenc) / derive_pt g c (Dg c Hopenc)) < - (2 * eps + 2)). intros eps0 Heps0. assert (Hdeb4: 2 * eps0 + 2 > 0) by lra. specialize (Hlimder (2 * eps0 + 2) Hdeb4). 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. specialize (H0 (eps) H). destruct H0 as [y [open H0]]. assert (Hdeb3 : 2 * eps + 2> 0) by lra. specialize (Hlimder (2 * eps + 2) Hdeb3). destruct Hlimder as [alp1 [Halp1 Hlim2]]. assert (Hdeb : 1 > 0) by lra. generalize (H15 (f y) (1) Hdeb). intros H16. destruct H16 as [alp2 [Halp2 Hlim3]]. assert (Hdeb2 : 1 / 2 > 0) by lra. generalize (H15 (g y) (1/2) Hdeb2). intros H16. destruct H16 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. apply Rmin_pos; assumption. unfold open_interval in H1. destruct H1. now lra. unfold open_interval in open. destruct open. now lra. destruct open; 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 H4. now lra. now destruct H1; lra. destruct H2. lra. destruct H2; lra. assert (open_interval a a' y). now apply open. specialize (Hacc2' H4 H5). assert (x < y). unfold alp in H3. unfold dist in H3. simpl in H3. unfold R_dist in H3. assert (Rabs (x - a) < Rabs (y - a)). rewrite (Rabs_right (y - a)). unfold alp in H3. apply Rlt_le_trans with (Rmin (Rmin alp_alp (a' - a)) (y - a)). now intuition. now apply Rmin_r. destruct H5. now lra. do 2 rewrite Rabs_right in H6. now lra. now destruct H5; lra. now destruct H4; lra. now destruct H4; lra. specialize (Hacc2' H6). destruct Hacc2' as [c [Hopenc H10]]. destruct H10 as [H10 H100]. rewrite H10. unfold Rdiv. apply Rlt_trans with ((1 - g y * / g x) * derive_pt f c (Df c Hopenc) * / derive_pt g c (Dg c Hopenc) + 1). rewrite Rmult_assoc. apply Rplus_lt_compat_l. specialize (Hlim3 x H2). assert (R_dist x a < alp2). 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 H3. now apply Rmin_l. now apply Rmin_l. now apply Rmin_l. now apply Rmin_r. specialize (Hlim3 H7). apply Rabs_def2 in Hlim3. apply Hlim3. apply Rlt_le_trans with (1 / 2 * (- (2 * eps + 2)) + 1). apply Rplus_lt_compat_r. apply Rlt_trans with ((1 - g y * / g x) * (- (2 * eps + 2))). rewrite Rmult_assoc. apply Rmult_lt_compat_l. replace 0 with (1 - 1). apply Rplus_lt_compat_l. apply Ropp_gt_lt_contravar. apply Rlt_trans with (1 / 2). assert (R_dist x a < alp3). 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)). apply H3. apply Rmin_l. apply Rmin_l. apply Rmin_r. specialize (Hlim4 x H2 H7). apply Rabs_def2. apply Hlim4. lra. ring. apply H0. split. apply Hopenc. apply H100. do 2 rewrite Ropp_mult_distr_r_reverse. apply Ropp_gt_lt_contravar. apply Rmult_lt_compat_r. intuition. replace (1 /2) with (1 - 1/ 2) by field. apply Rplus_lt_compat_l. apply Ropp_gt_lt_contravar. specialize (Hlim4 x H2). assert (R_dist x a < alp3). 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)). apply H3. apply Rmin_l. apply Rmin_l. apply Rmin_r. specialize (Hlim4 H7). apply Rabs_def2 in Hlim4. apply Hlim4. apply Req_le. field. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality