# Library Coqtail.Reals.Hopital

Require Import Reals.
Require Import Fourier.
Require Import Rfunction_classes_def.
Require Import Cauchy_lipschitz. Require Import Rextensionality.
Open Scope R_scope.

Definition derivable_on_interval a b (Hab : a < b) f :=
x, open_interval a b xderivable_pt f x.

Section Definitions.

Definition limit_div_pos f (I : RProp) a := m, m > 0 →
alp, alp > 0
x, I xR_dist x a < alpm < f x.

Definition limit_div_neg f (I : RProp) a := m, m > 0 →
alp, alp > 0
x, I xR_dist x a < alp-m > f x.

Lemma limit_div_Ropp : a b g, a < b
limit_div_neg g (open_interval a b) a
limit_div_pos (fun x : R- g x) (open_interval a b) a.
Proof.
intros. unfold limit_div_pos, limit_div_neg in ×. intros. specialize (H0 m H1).
destruct H0. x. split.
now intuition.

intros. destruct H0. specialize (H4 x0 H2 H3). fourier.
Qed.

Lemma limit_div_pos_inv : f a b, limit_div_neg (fun x- f x) (open_interval a b) a
limit_div_pos f (open_interval a b) a.
Proof.
intros.
unfold limit_div_pos, limit_div_neg in ×.
intros m Hm. specialize (H m Hm).
destruct H as [alp [Halp Hsolve]].
alp. split. assumption.
intros. specialize (Hsolve x H H0).
fourier.
Qed.

Lemma limit_div_neg_inv : f a b, limit_div_pos (fun x- f x) (open_interval a b) a
limit_div_neg f (open_interval a b) a.
Proof.
intros.
unfold limit_div_pos, limit_div_neg in ×.
intros m Hm. specialize (H m Hm).
destruct H as [alp [Halp Hsolve]].
alp. split. assumption.
intros. specialize (Hsolve x H H0).
fourier.
Qed.

Lemma limit_div_neg_ext : f g (I : RProp) a, ( x, I xf x = g x) →
limit_div_neg f I alimit_div_neg g I a.
Proof.
intros.
unfold limit_div_neg in ×.
intros m Hm. specialize (H0 m Hm).
destruct H0 as [alp [Halp Hsolve]].
alp. split. assumption.
intros. specialize (Hsolve x H0 H1).
rewrite <- H. apply Hsolve.
apply H0.
Qed.

Lemma limit_div_pos_ext : f g (I : RProp) a, ( x, I xf x = g x) →
limit_div_pos f I alimit_div_pos g I a.
Proof.
intros.
unfold limit_div_neg in ×.
intros m Hm. specialize (H0 m Hm).
destruct H0 as [alp [Halp Hsolve]].
alp. split. assumption.
intros. specialize (Hsolve x H0 H1).
rewrite <- H. apply Hsolve.
apply H0.
Qed.

Lemma limit_div_pos_open : a b b' f,
open_interval a b b'limit_div_pos f (open_interval a b') alimit_div_pos f (open_interval a b) a.
Proof.
intros.
unfold limit_div_pos in ×. intros m Hm.
destruct (H0 m Hm) as [alp [Halp Hsolve]].
(Rmin alp (b' - a)). split. apply Rmin_Rgt_r. split; destruct H; fourier.
intros. assert (x < b').
unfold R_dist in H2. rewrite Rabs_right in H2. replace b' with ((b' - a) + a) by ring.
assert (x - a < b' - a). apply Rlt_le_trans with (Rmin alp (b'- a)). apply H2.
apply Rmin_r. fourier. destruct H1; fourier.
apply Hsolve. split. apply H1. apply H3. apply Rlt_le_trans with (Rmin alp (b'-a)).
apply H2. apply Rmin_l.
Qed.

Lemma limit_div_neg_open : a b b' f,
open_interval a b b'limit_div_neg f (open_interval a b') alimit_div_neg f (open_interval a b) a.
Proof.
intros.
unfold limit_div_neg in ×. intros m Hm.
destruct (H0 m Hm) as [alp [Halp Hsolve]].
(Rmin alp (b' - a)). split. apply Rmin_Rgt_r. split; destruct H; fourier.
intros. assert (x < b').
unfold R_dist in H2. rewrite Rabs_right in H2. replace b' with ((b' - a) + a) by ring.
assert (x - a < b' - a). apply Rlt_le_trans with (Rmin alp (b'- a)). apply H2.
apply Rmin_r. fourier. destruct H1; fourier.
apply Hsolve. split. apply H1. apply H3. apply Rlt_le_trans with (Rmin alp (b'-a)).
apply H2. apply Rmin_l.
Qed.

Lemma limit_div_pos_opp : a b g, limit_div_pos g (open_interval a b) b
limit_div_pos (fun x : Rg (- x)) (open_interval (- b) (- a)) (- b).
Proof.
intros.
unfold limit_div_pos in ×.
intros m Hm. destruct (H m Hm) as [alp [Halp Hsolve]].
alp. split. apply Halp. intros.
assert (Hopen : open_interval a b (-x)). split; destruct H0; fourier.
assert (Hdist : R_dist (-x) b < alp). unfold R_dist in ×.
replace (-x - b) with (- (x + b)) by ring.
rewrite Rabs_Ropp. ring_simplify (x -- b) in H1. apply H1.
specialize (Hsolve (-x) Hopen Hdist).
apply Hsolve.
Qed.

Lemma limit_div_neg_opp : a b g, limit_div_neg g (open_interval a b) b
limit_div_neg (fun x : Rg (- x)) (open_interval (- b) (- a)) (- b).
Proof.
intros.
unfold limit_div_neg in ×.
intros m Hm. destruct (H m Hm) as [alp [Halp Hsolve]].
alp. split. apply Halp. intros.
assert (Hopen : open_interval a b (-x)). split; destruct H0; fourier.
assert (Hdist : R_dist (-x) b < alp). unfold R_dist in ×.
replace (-x - b) with (- (x + b)) by ring.
rewrite Rabs_Ropp. ring_simplify (x -- b) in H1. apply H1.
specialize (Hsolve (-x) Hopen Hdist).
apply Hsolve.
Qed.

Lemma limit_div_pos_imp :
(f : RR) (D D1 : RProp) (l : R),
( x0 : R, D1 x0D x0) → limit_div_pos f D llimit_div_pos f D1 l.
Proof.
intros.
unfold limit_div_pos in ×.
intros m Hm.
specialize (H0 m Hm).
destruct H0 as [alp [Halp Hsolve]].
alp. split.
apply Halp.
intros. assert (D x).
intuition.
specialize (Hsolve x H2 H1). apply Hsolve.
Qed.

Lemma limit_div_neg_imp :
(f : RR) (D D1 : RProp) (l : R),
( x0 : R, D1 x0D x0) → limit_div_neg f D llimit_div_neg f D1 l.
Proof.
intros.
intros m Hm.
specialize (H0 m Hm).
destruct H0 as [alp [Halp Hsolve]].
alp. split.
apply Halp.
intros. assert (D x).
intuition.
specialize (Hsolve x H2 H1). apply Hsolve.
Qed.

Lemma limit_div_pos_comp_Ropp :
(g : RR) (a b : R),
limit_div_pos g (open_interval (-a) (-b)) (-a) →
limit_div_pos (comp g (fun x-x)) (open_interval b a) a.
Proof.
intros.
intros m Hm.
specialize (H m Hm).
destruct H as [alp [Halp Hsolve]].
alp. split. apply Halp.
intros. specialize (Hsolve (-x)).
apply Hsolve. split; destruct H; fourier.
unfold R_dist in ×. replace (- x - - a) with (- (x - a)) by ring.
rewrite Rabs_Ropp. apply H0.
Qed.

Lemma limit_div_pos_comp_Ropp_l :
(g : RR) (a b : R),
limit_div_pos g (open_interval (-a) (-b)) (-b) →
limit_div_pos (comp g (fun x-x)) (open_interval b a) b.
Proof.
intros.
intros m Hm.
specialize (H m Hm).
destruct H as [alp [Halp Hsolve]].
alp. split. apply Halp.
intros. specialize (Hsolve (-x)).
apply Hsolve. split; destruct H; fourier.
unfold R_dist in ×. replace (- x - - b) with (- (x - b)) by ring.
rewrite Rabs_Ropp. apply H0.
Qed.

Lemma limit_div_neg_comp_Ropp :
(g : RR) (a b : R),
limit_div_neg g (open_interval (-a) (-b)) (-a) →
limit_div_neg (comp g (fun x-x)) (open_interval b a) a.
Proof.
intros.
intros m Hm.
specialize (H m Hm).
destruct H as [alp [Halp Hsolve]].
alp. split. apply Halp.
intros. specialize (Hsolve (-x)).
apply Hsolve. split; destruct H; fourier.
unfold R_dist in ×. replace (- x - - a) with (- (x - a)) by ring.
rewrite Rabs_Ropp. apply H0.
Qed.

Lemma limit_div_neg_comp_Ropp_l :
(g : RR) (a b : R),
limit_div_neg g (open_interval (-a) (-b)) (-b) →
limit_div_neg (comp g (fun x-x)) (open_interval b a) b.
Proof.
intros.
intros m Hm.
specialize (H m Hm).
destruct H as [alp [Halp Hsolve]].
alp. split. apply Halp.
intros. specialize (Hsolve (-x)).
apply Hsolve. split; destruct H; fourier.
unfold R_dist in ×. replace (- x - - b) with (- (x - b)) by ring.
rewrite Rabs_Ropp. apply H0.
Qed.

End Definitions.

Lemma derive_pt_comp_Ropp : a b f x (Df : x, open_interval a b xderivable_pt f x)
(Df' : x, open_interval (-b) (-a) xderivable_pt (fun x0f (- x0)) x)
(H1 : open_interval (-b) (-a) x) (H2 : open_interval a b (-x)), - derive_pt f (- x) (Df (- x) H2) =
derive_pt (fun x0 : Rf (- x0)) x (Df' x H1).
Proof.
intros.
assert (derivable_pt (comp f (fun xRopp x)) x). reg. apply derivable_pt_opp. reg.
apply Df. apply H2.

assert (Heq : x, (fun x0f (-x0)) x = (comp f (fun xRopp x)) x).
intros. reflexivity.

rewrite (derive_pt_ext (fun x0f (-x0)) (comp f (fun xRopp x)) Heq x (Df' (x) H1) H).
assert (derivable_pt (fun x ⇒ (-x)) x). reg.
assert (derivable_pt f ((fun x-x) x)). apply Df. apply H2.
pose (p := derivable_pt_comp (fun x ⇒ (-x)) f x H0 H3).
rewrite (pr_nu_var _ _ _ H p).
unfold p.
rewrite derive_pt_comp. replace (derive_pt (fun x0 : R ⇒ (- x0)%R) x H0) with (-1).
ring_simplify. apply Ropp_eq_compat. apply pr_nu.
rewrite <- derive_pt_id with x. rewrite <- derive_pt_opp.
unfold id. apply pr_nu.
reflexivity.
Qed.

Section FirstGenHopital.

Variables f g : RR.
Variables a b L : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).
Hypothesis (Zf : limit1_in f (open_interval a b) 0 a).
Hypothesis (Zg : limit1_in g (open_interval a b) 0 a).

Hypothesis (g_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0 g x 0).
Hypothesis (Hlimder : eps, eps > 0 →
alp,
alp > 0
( x (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)).

Lemma limit_open : f a b,
limit1_in f (D_x no_cond a) (f a) alimit1_in f (open_interval a b) (f a) a.
Proof.
clear Hlimder Zf Zg. unfold limit1_in in ×. unfold limit_in in ×. intros. specialize (H eps H0).
destruct H as [alp [Halp H2]]. alp. split.
now apply Halp.

intros. apply H2. destruct H. split.
constructor.
now constructor.

unfold open_interval in H. now intro; destruct H; fourier.

apply H1.
Qed.

Lemma f_a_zero : f a = 0.
Proof.
assert ( x (Hclose : a x b), continuity_pt f x).
intros. apply Cf. now apply Hclose.

unfold continuity_pt in H. unfold continue_in in H. specialize (H a). assert (a a b) by intuition.
apply H in H0. apply (limit_open f a b) in H0. eapply single_limit; [ | apply H0 | apply Zf ]. unfold adhDa.
intros. (a + Rmin ((b - a) / 2) (alp / 2)). assert (H6 : alp / 2 > 0) by fourier.
assert ((b - a) > 0) by fourier. assert ((b-a) /2 > 0).
apply (Rmult_gt_0_compat (/2)) in H2.
now fourier.

now fourier.

split.
unfold open_interval. split.
assert (Rmin ((b - a) /2) (alp/2) > 0).
apply Rmin_Rgt_r. now intuition.

now fourier.

apply Rle_lt_trans with (a + (b-a) / 2).
apply Rplus_le_compat.
now intuition.

now apply Rmin_l.

assert (b - a - (b - a) / 2 > 0).
field_simplify. now fourier.

now fourier.

unfold R_dist. rewrite Rabs_right.
ring_simplify. apply Rle_lt_trans with (alp / 2).
now apply Rmin_r.

now fourier.

ring_simplify. apply Rle_ge. apply Rmin_glb; intuition.
Qed.

Lemma g_a_zero : g a = 0.
Proof.
assert ( x (Hclose : a x b), continuity_pt g x).
intros. apply Cg. now apply Hclose.

unfold continuity_pt in H. unfold continue_in in H. specialize (H a). assert (a a b) by intuition.
apply H in H0. apply (limit_open g a b) in H0. eapply single_limit; [ | apply H0 | apply Zg ].
unfold adhDa. intros. (a + Rmin ((b - a) / 2) (alp / 2)). assert (H6 : alp / 2 > 0) by fourier.
assert ((b - a) > 0) by fourier. assert ((b-a) /2 > 0).
apply (Rmult_gt_0_compat (/2)) in H2.
now fourier.

now fourier.

split.
unfold open_interval. split.
assert (Rmin ((b - a) /2) (alp/2) > 0).
apply Rmin_Rgt_r. now intuition.

now fourier.

apply Rle_lt_trans with (a + (b-a) / 2).
apply Rplus_le_compat.
now intuition.

now apply Rmin_l.

assert (b - a - (b - a) / 2 > 0).
field_simplify. now fourier.

now fourier.

unfold R_dist. rewrite Rabs_right.
ring_simplify. apply Rle_lt_trans with (alp / 2).
now apply Rmin_r.

now fourier.

ring_simplify. apply Rle_ge. apply Rmin_glb; intuition.
Qed.

Theorem Hopital_g0_Lfin_right : limit1_in (fun xf x / g x) (open_interval a b) L a.
Proof.
unfold limit1_in, limit_in. intros. specialize (Hlimder eps H). destruct Hlimder as [alp [Halp Hlim]].
alp. split.
now assumption.

intros. assert (Hacc2 : x, open_interval a b x
c, 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 (H1 f g a x0). assert ( c, a < c < x0derivable_pt f c).
intros. apply Df. unfold open_interval. split.
now intuition.

now apply Rlt_trans with x0; unfold open_interval in H2; intuition.

assert ( c, a < c < x0derivable_pt g c).
intros. apply Dg. unfold open_interval. split.
now intuition.

now apply Rlt_trans with x0; unfold open_interval in H2; intuition.

specialize (H1 H3 H4). assert (a < x0) by (unfold open_interval in H2; intuition).
assert ( c : R, a c x0continuity_pt f c).
intros. apply Cf. split.
now intuition.

unfold open_interval in H2. now apply Rle_trans with x0; intuition.

assert ( c, a c x0continuity_pt g c).
intros. apply Cg. split.
now intuition.

unfold open_interval in H2. now apply Rle_trans with x0; intuition.

specialize (H1 H5 H6 H7). destruct H1 as [c [P Hold2]]. 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 H2.

Hopenc. split.
rewrite g_a_zero in Hold2. rewrite f_a_zero in Hold2. do 2 rewrite Rminus_0_r in Hold2.
apply (Rmult_eq_reg_l (g x0)).
rewrite (pr_nu f c _ (H3 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 H2).
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 H2.

now apply P.

destruct H0. specialize (Hacc2 x H0). destruct Hacc2 as [c [Hopenc Haccc]]. specialize (Hlim c).
simpl in ×. unfold R_dist in ×. assert (open_interval a b c Rabs (c - a) < alp).
split.
now apply Hopenc.

destruct Haccc. destruct H3. rewrite Rabs_right.
rewrite Rabs_right in H1.
now fourier.

now fourier.

now fourier.

specialize (Hlim Hopenc). destruct H2. specialize (Hlim H3). destruct Haccc. rewrite H4.
apply Hlim.
Qed.

End FirstGenHopital.

Section FirstGenHopital_left.

Variables f g : RR.
Variables a b L : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).
Hypothesis (Zf : limit1_in f (open_interval a b) 0 b).
Hypothesis (Zg : limit1_in g (open_interval a b) 0 b).

Hypothesis (g_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0 g x 0).
Hypothesis (Hlimder : eps, eps > 0 →
alp,
alp > 0
( x (Hopen : open_interval a b x), R_dist x b < alp
R_dist (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)) L < eps)).

Theorem Hopital_g0_Lfin_left : limit1_in (fun xf x / g x) (open_interval a b) L b.
Proof.
apply limit1_ext with (comp (fun xf (-x) / g (-x)) (fun x-x)).
intros. unfold comp. ring_simplify (--x). now reflexivity.

apply limit1_imp with (Dgf (open_interval a b) (open_interval (-b) (-a)) (fun x- x)).
intros. unfold Dgf. split.
now apply H.

now destruct H; split; fourier.

apply (limit_comp (fun x- x) (fun x : Rf (- x) / g (- x)) _ _ (-b)).
unfold limit1_in, limit_in. intros. eps. split.
now assumption.

intros. destruct H0. unfold dist in ×. simpl in ×. destruct H0. unfold R_dist in ×.
replace (- x -- b) with (- (x - b)) by ring. rewrite Rabs_Ropp. now apply H1.

assert (Df': x, open_interval (-b) (-a) xderivable_pt (fun xf (- x)) x).
intros. reg. apply Df. now destruct H; split; fourier.

assert (Dg': x, open_interval (-b) (-a) xderivable_pt (fun xg (- x)) x).
intros. reg. apply Dg. now destruct H; split; fourier.

apply Hopital_g0_Lfin_right with Df' Dg'.
now intuition.

intros. reg. apply Cf. now destruct H; split; fourier.

intros. reg. apply Cg. now destruct H; split; fourier.

unfold limit1_in, limit_in in ×. intros eps Heps. specialize (Zf eps Heps). destruct Zf as [alp [Halp Hsolve]].
alp. split.
now assumption.

intros x H. specialize (Hsolve (-x)). assert (H1 : open_interval a b (- x) dist R_met (- x) b < alp).
split.
destruct H. now destruct H; split; fourier.

unfold dist in ×. simpl in ×. destruct H. unfold R_dist in ×. replace (-x - b) with (- (x -- b)) by ring.
rewrite Rabs_Ropp. now apply H0.

apply Hsolve. now apply H1.

unfold limit1_in, limit_in in ×. intros eps Heps. specialize (Zg eps Heps). destruct Zg as [alp [Halp Hsolve]].
alp. split.
now assumption.

intros x H. specialize (Hsolve (-x)). assert (H1 : open_interval a b (- x) dist R_met (- x) b < alp).
split.
destruct H. now destruct H; split; fourier.

unfold dist in ×. simpl in ×. destruct H. unfold R_dist in ×. replace (-x - b) with (- (x -- b)) by ring.
rewrite Rabs_Ropp. now apply H0.

apply Hsolve. now apply H1.

intros. assert (Hopen2: open_interval a b (-x)).
now destruct Hopen; split; fourier.

destruct (g_not_0 (-x) Hopen2). split.
assert (derive_pt (fun x0 : Rg (- x0)) x (Dg' x Hopen) = - derive_pt g (- x) (Dg (- x) Hopen2)).
reg.
apply Ropp_eq_compat. now apply pr_nu.

apply Dg. now apply Hopen2.

rewrite H1. intro. apply H. replace 0 with (-0) in H2 by ring. apply Ropp_eq_compat in H2.
ring_simplify in H2. now apply H2.

now apply H0.

intros eps Heps. specialize (Hlimder eps Heps). destruct Hlimder as [alp [Halp Hsolve]].
alp. split.
now assumption.

intros. assert (open_interval a b (-x)).
now destruct Hopen; split; fourier.

assert (R_dist (-x) b < alp).
unfold R_dist in ×. replace (- x - b) with (- (x -- b)) by ring. rewrite Rabs_Ropp.
now apply H.

specialize (Hsolve (-x) H0 H1). assert (derive_pt (fun x0 : Rf (- x0)) x (Df' x Hopen) = - derive_pt f (- x) (Df (- x) H0) ).
reg.
apply Ropp_eq_compat. now apply pr_nu.

apply Df. now destruct Hopen; split; fourier.

assert (derive_pt (fun x0 : Rg (- x0)) x (Dg' x Hopen) = - derive_pt g (- x) (Dg (- x) H0) ).
reg.
apply Ropp_eq_compat. now apply pr_nu.

apply Dg. now destruct Hopen; split; fourier.

rewrite H2. rewrite H3. replace (- derive_pt f (- x) (Df (- x) H0) / - derive_pt g (- x) (Dg (- x) H0)) with
(derive_pt f (- x) (Df (- x) H0) / derive_pt g (- x) (Dg (- x) H0)).
now apply Hsolve.

field. apply g_not_0.
Qed.

End FirstGenHopital_left.

Section SndGenHopital.

Variables f g : RR.
Variables a b L : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).

Hypothesis (Zg : limit_div_pos g (open_interval a b) a).

Hypothesis (g'_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0).
Hypothesis (Hlimder : eps, eps > 0 →
alp,
alp > 0
( x (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)).

Lemma open_lemma : a b c, a < bc > 0 → open_interval a b (a + Rmin ((b - a) /2) c).
Proof.
intros. assert ((b0 - a0) > 0) by fourier. assert ((b0-a0) /2 > 0).
apply (Rmult_gt_0_compat (/2)) in H1.
now fourier.

now fourier.

split.
assert (Rmin ((b0-a0) /2) c > 0).
now apply Rmin_glb_lt; assumption.

now fourier.

apply Rle_lt_trans with (a0 + (b0-a0) /2).
apply Rplus_le_compat_l. now apply Rmin_l.

assert (b0 - a0 - (b0-a0) /2 > 0).
field_simplify. now fourier.

fourier.
Qed.

Lemma g_not_zero : a', open_interval a b a' x, open_interval a a' xg x 0.
Proof.
unfold limit_div_pos in Zg. assert (1 > 0) by fourier. specialize (Zg 1 H). destruct Zg as [alp [Halp H3]].
(a + Rmin ((b - a) / 2) (alp / 2)). assert (H6 : alp / 2 > 0) by fourier.
assert ((b - a) > 0) by fourier. assert ((b-a) /2 > 0).
apply (Rmult_gt_0_compat (/2)) in H0.
now fourier.

now fourier.

split.
unfold open_interval. split.
assert (Rmin ((b-a) /2) (alp / 2) > 0).
now apply Rmin_glb_lt; assumption.

now fourier.

apply Rle_lt_trans with (a + (b-a) /2).
apply Rplus_le_compat_l. now apply Rmin_l.

assert (b - a - (b-a) /2 > 0).
field_simplify. now fourier.

now fourier.

intros. unfold open_interval in H0. assert (g x > 1).
apply H3.
unfold open_interval. unfold open_interval in H2. split.
now apply H2.

apply Rlt_trans with (a + Rmin ((b-a)/2) (alp /2)).
now apply H2.

apply Rle_lt_trans with (a + (b-a) /2).
apply Rplus_le_compat_l. now apply Rmin_l.

assert (b - a - (b-a) /2 > 0).
field_simplify. now fourier.

now fourier.

unfold R_dist. unfold open_interval in H2. destruct H2. apply Rlt_trans with (alp/2).
apply Rlt_le_trans with (Rmin ((b-a) / 2) (alp /2)).
now rewrite Rabs_right; fourier.

now apply Rmin_r.

now fourier.

intro. fourier.
Qed.

Lemma MVT_unusable : a', open_interval a b a'
x y : R,
open_interval a a' x
open_interval a a' y
x < y
c : R,
Hopenc : open_interval a b c,
(f y - f x) × derive_pt g c (Dg c Hopenc) =
derive_pt f c (Df c Hopenc) × (g y - g x)
x < c < y.
Proof.
intros a' Hopennew. generalize MVT. intros. specialize (H f g x y). assert ( c, x < c < yderivable_pt f c).
intros. apply Df. unfold open_interval in ×. split.
now apply Rlt_trans with x ; intuition.

apply Rlt_trans with y ; intuition. now apply Rlt_trans with a'; intuition.

assert ( c, x < c < yderivable_pt g c).
intros. apply Dg. unfold open_interval in ×. split.
now apply Rlt_trans with x ; intuition.

apply Rlt_trans with y ; intuition. now apply Rlt_trans with a'; intuition.

specialize (H H3 H4 H2). assert ( c : R, x c ycontinuity_pt f c).
intros. apply Cf. unfold open_interval in ×. split.
now apply Rle_trans with x; intuition.

apply Rle_trans with y; intuition. now apply Rle_trans with a'; intuition.

assert ( c : R, x c ycontinuity_pt g c).
intros. apply Cg. unfold open_interval in ×. split.
now apply Rle_trans with x; intuition.

apply Rle_trans with y; intuition. now apply Rle_trans with a'; intuition.

specialize (H H5 H6). destruct H as [c [P Hold2]]. c. assert (Hopenc : open_interval a b c).
unfold open_interval in ×. destruct P; split.
now apply Rlt_trans with x; intuition.

apply Rlt_trans with y; intuition. now apply Rlt_trans with a'; intuition.

Hopenc. split.
rewrite (pr_nu f c _ (H3 c P)). rewrite (pr_nu g c _ (H4 c P)). rewrite <- Hold2.
now ring.

apply P.
Qed.

Theorem Hopital_gpinf_Lfin_right : limit1_in (fun xf x / g x) (open_interval a b) L a.
Proof.
destruct g_not_zero as [a' [H1 Ha']]. unfold limit1_in, limit_in. intros. assert (Hacc2' : x y, open_interval a a' xopen_interval a a' yx < y
c, 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]]].
c. 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 fourier.

now apply g'_not_0.

now apply Ha'; assumption.

assert (H0: eps, eps > 0 →
y, open_interval a a' y 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]].
(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; fourier.

now apply Rmin_r.

assert (H15 : A eps, eps > 0 → alp,
alp > 0 x, open_interval a b xR_dist x a < alpRabs (A / g x) < eps).
intros. unfold limit_div_pos in Zg. destruct (Req_dec A 0) as [eq_dec1 | eq_dec2].
subst. 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]]. 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. rewrite Rinv_1. rewrite Rmult_1_r. now apply Zg3.

intro. now fourier.

split.
intro. now fourier.

intro. now fourier.

now fourier.

intro. now fourier.

assert (Heps4 : eps / 4 > 0) by fourier. assert (bizarre : eps L, L 0 → eps > 0 →
eps1, eps1 > 0 eps1 × (L + eps) < eps / 2).
intros. (/2 × ((eps0 / 2) × / (L0 + eps0))). split.
apply Rmult_lt_0_compat.
now fourier.

apply Rmult_lt_0_compat.
now fourier.

apply Rinv_0_lt_compat. now fourier.

field_simplify.
now fourier.

intro. now fourier.

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)).
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 fourier.

unfold open_interval in open. destruct open. now fourier.

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 fourier.

do 2 rewrite Rabs_right in H3.
now fourier.

now destruct H1; fourier.

destruct H2. now destruct H2; fourier.

destruct H2. now destruct H2; fourier.

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 fourier.

do 2 rewrite Rabs_right in H5.
now fourier.

now destruct H4; fourier.

now destruct H3; fourier.

now destruct H3; fourier.

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 fourier.

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.

End SndGenHopital.

Section SndGenHopital_left.

Variables f g : RR.
Variables a b L : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).

Hypothesis (Zg : limit_div_pos g (open_interval a b) b).

Hypothesis (g'_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0).
Hypothesis (Hlimder : eps, eps > 0 →
alp,
alp > 0
( x (Hopen : open_interval a b x), R_dist x b < alp
R_dist (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)) L < eps)).

Theorem Hopital_gpinf_Lfin_left : limit1_in (fun xf x / g x) (open_interval a b) L b.
Proof.
apply limit1_ext with (comp (fun xf (-x) / g (-x)) (fun x-x)).
intros. unfold comp. ring_simplify (--x). now reflexivity.

apply limit1_imp with (Dgf (open_interval a b) (open_interval (-b) (-a)) (fun x- x)).
intros. unfold Dgf. split.
now apply H.

now destruct H; split; fourier.

apply (limit_comp (fun x- x) (fun x : Rf (- x) / g (- x)) _ _ (-b)).
unfold limit1_in, limit_in. intros. eps. split.
now assumption.

intros. destruct H0. unfold dist in ×. simpl in ×. destruct H0. unfold R_dist in ×.
replace (- x -- b) with (- (x - b)) by ring. rewrite Rabs_Ropp. now apply H1.

assert (Df': x, open_interval (-b) (-a) xderivable_pt (fun xf (- x)) x).
intros. reg. apply Df. now destruct H; split; fourier.

assert (Dg': x, open_interval (-b) (-a) xderivable_pt (fun xg (- x)) x).
intros. reg. apply Dg. now destruct H; split; fourier.

apply Hopital_gpinf_Lfin_right with Df' Dg'.
now intuition.

intros. reg. apply Cf. now destruct H; split; fourier.

intros. reg. apply Cg. now destruct H; split; fourier.

apply limit_div_pos_opp. apply Zg.

intros.

intros. assert (Hopen2: open_interval a b (-x)).
now destruct Hopen; split; fourier.

intro. destruct (g'_not_0 (-x) Hopen2).
assert (derive_pt (fun x0 : Rg (- x0)) x (Dg' x Hopen) = - derive_pt g (- x) (Dg (- x) Hopen2)).
reg.
apply Ropp_eq_compat. now apply pr_nu.

apply Dg. now apply Hopen2.

rewrite <- Ropp_involutive. symmetry. rewrite <- Ropp_involutive.
replace 0 with (- 0) in H by ring.
apply Ropp_eq_compat. rewrite <- H. rewrite H0. reflexivity.

intros eps Heps. specialize (Hlimder eps Heps).
destruct Hlimder as [alp [Halp Hsolve]].
alp. split. apply Halp.
intros.
assert (Hopenx : open_interval a b (-x)). split; destruct Hopen; fourier.
assert (R_dist (-x) b < alp). unfold R_dist in ×.
replace (- x - b) with (- (x + b)) by ring.
ring_simplify (x--b) in H.
rewrite Rabs_Ropp. apply H.
specialize (Hsolve (-x) Hopenx H0).
replace (derive_pt (fun x0 : Rf (- x0)) x (Df' x Hopen)) with
(- derive_pt f (- x) (Df (- x) Hopenx)).
replace (derive_pt (fun x0 : Rg (- 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 Hsolve.

field. apply g'_not_0.

apply derive_pt_comp_Ropp.
apply derive_pt_comp_Ropp.
Qed.

End SndGenHopital_left.

Section SndGenHopitalposneg.

Lemma g_not_zero2 : g a b, b > alimit_div_neg g (open_interval a b) a
a', open_interval a b a' x, open_interval a a' xg x 0.
Proof.
intros g a b Hab Zg. unfold limit_div_neg in Zg. assert (1 > 0) by fourier. specialize (Zg 1 H).
destruct Zg as [alp [Halp H3]]. (a + Rmin ((b - a) / 2) (alp / 2)). assert (H6 : alp / 2 > 0) by fourier.
assert ((b - a) > 0) by fourier. assert ((b-a) /2 > 0).
apply (Rmult_gt_0_compat (/2)) in H0.
now fourier.

now fourier.

split.
unfold open_interval. split.
assert (Rmin ((b-a) /2) (alp / 2) > 0).
now apply Rmin_glb_lt; assumption.

now fourier.

apply Rle_lt_trans with (a + (b-a) /2).
apply Rplus_le_compat_l. now apply Rmin_l.

assert (b - a - (b-a) /2 > 0).
field_simplify. now fourier.

now fourier.

intros. unfold open_interval in H0. assert (g x < - 1).
apply H3.
unfold open_interval. unfold open_interval in H2. split.
now apply H2.

apply Rlt_trans with (a + Rmin ((b-a)/2) (alp /2)).
now apply H2.

apply Rle_lt_trans with (a + (b-a) /2).
apply Rplus_le_compat_l. now apply Rmin_l.

assert (b - a - (b-a) /2 > 0).
field_simplify. now fourier.

now fourier.

unfold R_dist. unfold open_interval in H2. destruct H2. apply Rlt_trans with (alp/2).
apply Rlt_le_trans with (Rmin ((b-a) / 2) (alp /2)).
now rewrite Rabs_right; fourier.

now apply Rmin_r.

now fourier.

intro. fourier.
Qed.

Lemma limit1_in_open : f L a b c, open_interval a b c
limit1_in f (open_interval a c) L a
limit1_in f (open_interval a b) L a.
Proof.
intros. unfold limit1_in in ×. unfold limit_in in ×. intros. specialize (H0 eps H1).
destruct H0 as [alp [Halp Hlim]]. (Rmin alp (c - a)). split.
apply Rmin_glb_lt.
now assumption.

now destruct H; fourier.

intros. apply Hlim. destruct H0. unfold dist in ×. simpl in ×. unfold R_dist in ×.
split.
split.
now destruct H0; assumption.

assert (Rabs (x - a) < c - a).
apply Rlt_le_trans with (Rmin alp (c - a)).
now apply H2.

now apply Rmin_r.

now rewrite Rabs_right in H3; destruct H0; fourier.

apply Rlt_le_trans with (Rmin alp (c - a)).
now apply H2.

apply Rmin_l.
Qed.

Lemma limit_div_neg_open1 : f a b c, open_interval a b c
limit_div_neg f (open_interval a b) a
limit_div_neg f (open_interval a c) a.
Proof.
intros. unfold limit_div_neg in ×. intros. specialize (H0 m H1). destruct H0 as [alp [Halp Hlim]].
alp. intuition. apply Hlim.
now destruct H; destruct H0; split; fourier.

apply H2.
Qed.

Lemma Hopital_gninf_Lfin_right
: (f g : RR) (a b L : R),
a < b
(Df : x : R, open_interval a b xderivable_pt f x)
(Dg : x : R, open_interval a b xderivable_pt g x),
( x : R, a x bcontinuity_pt f x) →
( x : R, a x bcontinuity_pt g x) →
limit_div_neg g (open_interval a b) a
( (x : R) (Hopen : open_interval a b x),
derive_pt g x (Dg x Hopen) 0) →
( eps : R,
eps > 0 →
alp : R,
alp > 0
( (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 : Rf x / g x) (open_interval a b) L a.
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' : x : R, open_interval a a' xderivable_pt (- g) x).
intros. reg. apply Dg. split.
now apply H5.

apply Rlt_trans with a'.
now apply H5.

now apply Hopen.

assert (Df' : x : R, open_interval a a' xderivable_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'' : x, open_interval a a' xderivable_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; fourier.

rewrite (pr_nu g x _ (Dg x Hder)). now apply H3.

intros. specialize (H4 eps H5). destruct H4 as [alp [Halp H10]]. alp. split.
now assumption.

intros. assert (Hder : open_interval a b x).
unfold open_interval in ×. split.
now apply Hopen0.

now destruct Hopen, Hopen0; fourier.

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'' : x, open_interval a a' xderivable_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.

End SndGenHopitalposneg.

Section SndGenHopitalposneg_left.

Lemma Hopital_gninf_Lfin_left
: (f g : RR) (a b L : R),
a < b
(Df : x : R, open_interval a b xderivable_pt f x)
(Dg : x : R, open_interval a b xderivable_pt g x),
( x : R, a x bcontinuity_pt f x) →
( x : R, a x bcontinuity_pt g x) →
limit_div_neg g (open_interval a b) b
( (x : R) (Hopen : open_interval a b x),
derive_pt g x (Dg x Hopen) 0) →
( eps : R,
eps > 0 →
alp : R,
alp > 0
( (x : R) (Hopen : open_interval a b x),
R_dist x b < alp
R_dist (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)) L <
eps)) →
limit1_in (fun x : Rf x / g x) (open_interval a b) L b.
Proof.
intros f g a b L Hab Df Dg Cf Cg Hdiv_neg g'_not_0 Hlimder.
apply limit1_ext with (comp (fun xf (-x) / g (-x)) (fun x-x)).
intros. unfold comp. ring_simplify (--x). now reflexivity.

apply limit1_imp with (Dgf (open_interval a b) (open_interval (-b) (-a)) (fun x- x)).
intros. unfold Dgf. split.
now apply H.

now destruct H; split; fourier.

apply (limit_comp (fun x- x) (fun x : Rf (- x) / g (- x)) _ _ (-b)).
unfold limit1_in, limit_in. intros. eps. split.
now assumption.

intros. destruct H0. unfold dist in ×. simpl in ×. destruct H0. unfold R_dist in ×.
replace (- x -- b) with (- (x - b)) by ring. rewrite Rabs_Ropp. now apply H1.

assert (Df': x, open_interval (-b) (-a) xderivable_pt (fun xf (- x)) x).
intros. reg. apply Df. now destruct H; split; fourier.

assert (Dg': x, open_interval (-b) (-a) xderivable_pt (fun xg (- x)) x).
intros. reg. apply Dg. now destruct H; split; fourier.

apply Hopital_gninf_Lfin_right with Df' Dg'.
now intuition.

intros. reg. apply Cf. now destruct H; split; fourier.

intros. reg. apply Cg. now destruct H; split; fourier.

apply limit_div_neg_opp. apply Hdiv_neg.

intros.

intros. assert (Hopen2: open_interval a b (-x)).
now destruct Hopen; split; fourier.

intro. destruct (g'_not_0 (-x) Hopen2).
assert (derive_pt (fun x0 : Rg (- x0)) x (Dg' x Hopen) = - derive_pt g (- x) (Dg (- x) Hopen2)).
reg.
apply Ropp_eq_compat. now apply pr_nu.

apply Dg. now apply Hopen2.

rewrite <- Ropp_involutive. symmetry. rewrite <- Ropp_involutive.
replace 0 with (- 0) in H by ring.
apply Ropp_eq_compat. rewrite <- H. rewrite H0. reflexivity.

intros eps Heps. specialize (Hlimder eps Heps).
destruct Hlimder as [alp [Halp Hsolve]].
alp. split. apply Halp.
intros.
assert (Hopenx : open_interval a b (-x)). split; destruct Hopen; fourier.
assert (R_dist (-x) b < alp). unfold R_dist in ×.
replace (- x - b) with (- (x + b)) by ring.
ring_simplify (x--b) in H.
rewrite Rabs_Ropp. apply H.
specialize (Hsolve (-x) Hopenx H0).
replace (derive_pt (fun x0 : Rf (- x0)) x (Df' x Hopen)) with
(- derive_pt f (- x) (Df (- x) Hopenx)).
replace (derive_pt (fun x0 : Rg (- 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 Hsolve.

field. apply g'_not_0.

apply derive_pt_comp_Ropp.
apply derive_pt_comp_Ropp.
Qed.

End SndGenHopitalposneg_left.

Section InfiniteLimiteHopital_pos.

Variables f g : RR.
Variables a b L : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).
Hypothesis (Zf : limit1_in f (open_interval a b) 0 a).
Hypothesis (Zg : limit1_in g (open_interval a b) 0 a).

Hypothesis (g_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0 g x 0).
Hypothesis (Hlimder : m, m > 0 →
alp,
alp > 0
( x (Hopen: open_interval a b x), R_dist x a < alp
m < (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)))).

Lemma Hopital_g0_Lpinf_right : m, m > 0 →
alp,
alp > 0
( x (Hopen: open_interval a b x), R_dist x a < alp
m < (f x) / (g x)).
Proof.
intros m Hm. specialize (Hlimder m Hm). destruct Hlimder as [alp [Halp Hlim]].
alp. split.
now assumption.

intros. assert (Hacc2 : x, open_interval a b x
c, 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 ( c, a < c < x0derivable_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 ( c, a < c < x0derivable_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 ( c : R, a c x0continuity_pt f c).
intros. apply Cf. split.
now intuition.

unfold open_interval in H1. now apply Rle_trans with x0; intuition.

assert ( c, a c x0continuity_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]]. 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.

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 fourier.

now fourier.

now fourier.

destruct H0. specialize (Hlim H1). destruct Haccc. rewrite H2.
apply Hlim.
Qed.

End InfiniteLimiteHopital_pos.

Section InfiniteLimiteHopital_pos_left.

Variables f g : RR.
Variables a b L : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).
Hypothesis (Zf : limit1_in f (open_interval a b) 0 b).
Hypothesis (Zg : limit1_in g (open_interval a b) 0 b).

Hypothesis (g_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0 g x 0).
Hypothesis (Hlimder : m, m > 0 →
alp,
alp > 0
( x (Hopen: open_interval a b x), R_dist x b < alp
m < (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)))).

Lemma Hopital_g0_Lpinf_left : limit_div_pos (fun xf x / g x) (open_interval a b) b.
Proof.
apply limit_div_pos_ext with (comp (fun xf (- x) / g (- x)) (fun x-x)).
intros. unfold comp. ring_simplify (--x). reflexivity.
apply limit_div_pos_comp_Ropp.
assert (Df': x, open_interval (-b) (-a) xderivable_pt (fun xf (- x)) x).
intros. reg. apply Df. now destruct H; split; fourier.

assert (Dg': x, open_interval (-b) (-a) xderivable_pt (fun xg (- x)) x).
intros. reg. apply Dg. now destruct H; split; fourier.
intros m Hm.
apply Hopital_g0_Lpinf_right with Df' Dg'.
now intuition.

intros. reg. apply Cf. now destruct H; split; fourier.

intros. reg. apply Cg. now destruct H; split; fourier.

apply limit1_ext with (comp f (fun x-x)). intros. reflexivity.
apply limit1_imp with (Dgf (open_interval (-b) (-a)) (open_interval a b) (fun x- x)).
intros. split. apply H. destruct H; split; fourier.
apply (limit_comp _ f _ _ b). unfold limit1_in, limit_in.
intros. eps. split. intuition. intros. simpl in ×. unfold R_dist in ×.
ring_simplify (x -- b) in H0. replace (- x - b) with (- (x + b)) by ring. rewrite Rabs_Ropp.
apply H0. apply Zf.

apply limit1_ext with (comp g (fun x-x)). intros. reflexivity.
apply limit1_imp with (Dgf (open_interval (-b) (-a)) (open_interval a b) (fun x- x)).
intros. split. apply H. destruct H; split; fourier.
apply (limit_comp _ g _ _ b). unfold limit1_in, limit_in.
intros. eps. split. intuition. intros. simpl in ×. unfold R_dist in ×.
ring_simplify (x -- b) in H0. replace (- x - b) with (- (x + b)) by ring. rewrite Rabs_Ropp.
apply H0. apply Zg.

intros. split.
assert (Hopen' : open_interval a b (-x)). split; destruct Hopen; fourier.
generalize (g_not_0 (-x) Hopen'). intros. intro. destruct H. destruct H.
erewrite <- (derive_pt_comp_Ropp a b g x Dg Dg' _ Hopen') in H0. replace 0 with (-0) by ring.
rewrite <- H0. ring.

apply g_not_0. split; destruct Hopen; fourier.

intros m1 Hm1. specialize (Hlimder m1 Hm1).
destruct Hlimder as [alp [Halp Hsolve1]].
alp. split. apply Halp.
intros.
assert (Hopenx : open_interval a b (-x)). destruct Hopen; split; fourier.
replace (derive_pt (fun x0 : Rf (- x0)) x (Df' x Hopen)) with
(- derive_pt f (- x) (Df (- x) Hopenx)).
replace (derive_pt (fun x0 : Rg (- 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.
apply Hm.
Qed.

End InfiniteLimiteHopital_pos_left.

Section InfiniteLimiteHopital_neg.

Variables f g : RR.
Variables a b L : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).
Hypothesis (Zf : limit1_in f (open_interval a b) 0 a).
Hypothesis (Zg : limit1_in g (open_interval a b) 0 a).

Hypothesis (g_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0 g x 0).
Hypothesis (Hlimder : m, m < 0 →
alp,
alp > 0
( x (Hopen: open_interval a b x), R_dist x a < alp
m > (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)))).

Lemma Hopital_g0_Lninf_right : m, m < 0 →
alp,
alp > 0
( x (Hopen: open_interval a b x), R_dist x a < alp
m > (f x) / (g x)).
Proof.
intros m Hm. specialize (Hlimder m Hm). destruct Hlimder as [alp [Halp Hlim]].
alp. split.
now assumption.

intros. assert (Hacc2 : x, open_interval a b x
c, 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 ( c, a < c < x0derivable_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 ( c, a < c < x0derivable_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 ( c : R, a c x0continuity_pt f c).
intros. apply Cf. split.
now intuition.

unfold open_interval in H1. now apply Rle_trans with x0; intuition.

assert ( c, a c x0continuity_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]]. 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.

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 fourier.

now fourier.

now fourier.

destruct H0. specialize (Hlim H1). destruct Haccc. rewrite H2.
apply Hlim.
Qed.

End InfiniteLimiteHopital_neg.

Section InfiniteLimiteHopital_neg_left.

Variables f g : RR.
Variables a b L : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).
Hypothesis (Zf : limit1_in f (open_interval a b) 0 b).
Hypothesis (Zg : limit1_in g (open_interval a b) 0 b).

Hypothesis (g_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0 g x 0).
Hypothesis (Hlimder : m, m < 0 →
alp,
alp > 0
( x (Hopen: open_interval a b x), R_dist x b < alp
m > (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)))).

Lemma Hopital_g0_Lninf_left : limit_div_neg (fun xf x / g x) (open_interval a b) b.
Proof.
apply limit_div_neg_ext with (comp (fun xf (- x) / g (- x)) (fun x-x)).
intros. unfold comp. ring_simplify (--x). reflexivity.
apply limit_div_neg_comp_Ropp.
assert (Df': x, open_interval (-b) (-a) xderivable_pt (fun xf (- x)) x).
intros. reg. apply Df. now destruct H; split; fourier.

assert (Dg': x, open_interval (-b) (-a) xderivable_pt (fun xg (- x)) x).
intros. reg. apply Dg. now destruct H; split; fourier.
intros m Hm.
apply Hopital_g0_Lninf_right with Df' Dg'.
now intuition.

intros. reg. apply Cf. now destruct H; split; fourier.

intros. reg. apply Cg. now destruct H; split; fourier.

apply limit1_ext with (comp f (fun x-x)). intros. reflexivity.
apply limit1_imp with (Dgf (open_interval (-b) (-a)) (open_interval a b) (fun x- x)).
intros. split. apply H. destruct H; split; fourier.
apply (limit_comp _ f _ _ b). unfold limit1_in, limit_in.
intros. eps. split. intuition. intros. simpl in ×. unfold R_dist in ×.
ring_simplify (x -- b) in H0. replace (- x - b) with (- (x + b)) by ring. rewrite Rabs_Ropp.
apply H0. apply Zf.

apply limit1_ext with (comp g (fun x-x)). intros. reflexivity.
apply limit1_imp with (Dgf (open_interval (-b) (-a)) (open_interval a b) (fun x- x)).
intros. split. apply H. destruct H; split; fourier.
apply (limit_comp _ g _ _ b). unfold limit1_in, limit_in.
intros. eps. split. intuition. intros. simpl in ×. unfold R_dist in ×.
ring_simplify (x -- b) in H0. replace (- x - b) with (- (x + b)) by ring. rewrite Rabs_Ropp.
apply H0. apply Zg.

intros. split.
assert (Hopen' : open_interval a b (-x)). split; destruct Hopen; fourier.
generalize (g_not_0 (-x) Hopen'). intros. intro. destruct H. destruct H.
erewrite <- (derive_pt_comp_Ropp a b g x Dg Dg' _ Hopen') in H0. replace 0 with (-0) by ring.
rewrite <- H0. ring.

apply g_not_0. split; destruct Hopen; fourier.

intros m1 Hm1. specialize (Hlimder m1 Hm1).
destruct Hlimder as [alp [Halp Hsolve1]].
alp. split. apply Halp.
intros.
assert (Hopenx : open_interval a b (-x)). destruct Hopen; split; fourier.
replace (derive_pt (fun x0 : Rf (- x0)) x (Df' x Hopen)) with
(- derive_pt f (- x) (Df (- x) Hopenx)).
replace (derive_pt (fun x0 : Rg (- 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.
fourier.
Qed.

End InfiniteLimiteHopital_neg_left.

Section Hopital_infinite_pos.

Variables f g : RR.
Variables a b : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).

Hypothesis (Zg : limit_div_pos g (open_interval a b) a).

Hypothesis (g'_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0).
Hypothesis (Hlimder : m, m > 0 →
alp,
alp > 0
( x (Hopen : open_interval a b x), R_dist x a < alp
(derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen) > m))).

Theorem Hopital_gpinf_Lpinf_right : limit_div_pos (fun xf x / g x) (open_interval a b) a.
Proof.
destruct (g_not_zero g a b Hab Zg) as [a' [H1 Ha']]. unfold limit_div_pos. intros eps H. assert (Hacc2' : x y, open_interval a a' xopen_interval a a' yx < y
c, 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]]].
c. 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 fourier.

now apply g'_not_0.

now apply Ha'; assumption.

assert (H0: eps, eps > 0 →
y, open_interval a a' y 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 fourier. specialize (Hlimder (2 × eps0 + 2) Hdeb4). destruct Hlimder as [alp [Halp Hlimder1]].
(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; fourier.

now apply Rmin_r.

assert (H15 : A eps, eps > 0 → alp,
alp > 0 x, open_interval a b xR_dist x a < alpRabs (A / g x) < eps).
intros. unfold limit_div_pos in Zg. destruct (Req_dec A 0) as [eq_dec1 | eq_dec2].
subst. 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]]. 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. rewrite Rinv_1. rewrite Rmult_1_r. now apply Zg3.

intro. now fourier.

split.
intro. now fourier.

intro. now fourier.

now fourier.

intro. now fourier.

specialize (H0 (eps) H). destruct H0 as [y [open H0]]. assert (Hdeb3 : 2 × eps + 2> 0) by fourier.
specialize (Hlimder (2 × eps + 2) Hdeb3).
destruct Hlimder as [alp1 [Halp1 Hlim2]]. assert (Hdeb : 1 > 0) by fourier. generalize (H15 (f y) (1) Hdeb).
intros H16. destruct H16 as [alp2 [Halp2 Hlim3]].
assert (Hdeb2 : 1 / 2 > 0) by fourier.
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)).
alp. split.
apply Rmin_pos.
apply Rmin_pos.
apply Rmin_pos.
apply Rmin_pos; assumption.

unfold open_interval in H1. destruct H1. now fourier.

unfold open_interval in open. destruct open. now fourier.
destruct open; fourier.

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 fourier.

do 2 rewrite Rabs_right in H4.
now fourier.

now destruct H1; fourier.

destruct H2. fourier. destruct H2; fourier.

assert (open_interval a a' y).
now apply open.

specialize (Hacc2' H4 H5). 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 H5. now fourier.

do 2 rewrite Rabs_right in H6.
now fourier.

now destruct H5; fourier.

now destruct H4; fourier.

now destruct H4; fourier.

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 Rle_lt_trans with ((1 / 2) × (2 × eps + 2) - 1).
replace (1 / 2 × (2 × eps + 2) - 1) with eps. intuition.
field.
unfold Rminus.
apply Rplus_lt_compat_r.
apply Rlt_trans with (1 / 2 *(derive_pt f c (Df c Hopenc) × / derive_pt g c (Dg c Hopenc)) ).
apply Rmult_lt_compat_l. fourier.
apply H0.
split. apply Hopenc. apply H100.

apply Rmult_lt_compat_r. apply Rlt_trans with (2 × eps + 2). fourier.
apply H0.
split. apply Hopenc. apply H100.

assert (HH : 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)).
now apply H3.

now apply Rmin_l.

now apply Rmin_l.

now apply Rmin_r.

specialize (Hlim4 x H2 HH). apply Rabs_def2 in Hlim4.
apply Rle_lt_trans with (1 - 1/2). fourier. unfold Rminus.
apply Rplus_lt_compat_l. destruct Hlim4. intuition.
apply Rplus_lt_compat_l.
assert (HH : 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 x H2 HH).
apply Rabs_def2 in Hlim3. intuition.
Qed.

End Hopital_infinite_pos.

Section Hopital_infinite_pos_left.

Variables f g : RR.
Variables a b : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).

Hypothesis (Zg : limit_div_pos g (open_interval a b) b).

Hypothesis (g'_not_0 : x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) 0).
Hypothesis (Hlimder : m, m > 0 →
alp,
alp > 0
( x (Hopen : open_interval a b x), R_dist x b < alp
(derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen) > m))).

Theorem Hopital_gpinf_Lpinf_left : limit_div_pos (fun xf x / g x) (open_interval a b) b.
Proof.
apply limit_div_pos_ext with (comp (fun xf (- x) / g (- x)) (fun x-x)).
intros. unfold comp. ring_simplify (--x). reflexivity.
apply limit_div_pos_comp_Ropp.
assert (Df': x, open_interval (-b) (-a) xderivable_pt (fun xf (- x)) x).
intros. reg. apply Df. now destruct H; split; fourier.

assert (Dg': x, open_interval (-b) (-a) xderivable_pt (fun xg (- x)) x).
intros. reg. apply Dg. now destruct H; split; fourier.
intros m Hm.
apply Hopital_gpinf_Lpinf_right with Df' Dg'.
now intuition.

intros. reg. apply Cf. now destruct H; split; fourier.

intros. reg. apply Cg. now destruct H; split; fourier.

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; fourier.
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]].
alp. split. apply Halp.
intros.
assert (Hopenx : open_interval a b (-x)). destruct Hopen; split; fourier.
replace (derive_pt (fun x0 : Rf (- x0)) x (Df' x Hopen)) with
(- derive_pt f (- x) (Df (- x) Hopenx)).
replace (derive_pt (fun x0 : Rg (- 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.
fourier.
Qed.

End Hopital_infinite_pos_left.

Section Hopital_infinite_neg.

Variables f g : RR.
Variables a b : R.

Hypothesis Hab : a < b.
Hypotheses (Df : x, open_interval a b xderivable_pt f x)
(Dg : x, open_interval a b xderivable_pt g x).
Hypotheses (Cf : x, a x bcontinuity_pt f x)
(Cg : x, a x bcontinuity_pt g x).

Hypothesis (Zg : limit_div_pos g (open_interval a b) a).

Hypothesis (g'_not_0 : x (Hopen: open_interval a