use L'Hopital's rule from MathComp 1.9.0

[affeldt-aist]

The rules from MathComp should be reusable directly.

I record here the glue that prove the old lemmas using the new ones (use only in case of emergency):

Section lhopital0.
Context {R : realType}.
Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U).
Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x))
           (gdg : forall x, x \in U -> is_derive x 1 g (dg x)).
Hypotheses (fa0 : f a = 0) (ga0 : g a = 0)
           (cdg : \forall x \near a^', dg x != 0).

Lemma lhopital_right (l : R) :
  df x / dg x @[x --> a^'+] --> l -> f x / g x @[x --> a^'+] --> l.
Proof.
case: Ua => e/= e0 aeU.
case: cdg => d/= d0 cdg'.
pose D := minr e d.
have := @lhopital_at_right R f df g dg a (a + D).
rewrite ltrDl.
have D0 : 0 < D by rewrite lt_min e0 d0.
move=> /(_ _ D0).
have H (x : R) (G : R) : 0 < G -> x \in `]a, (a + G)%E[ -> `|a - x| < G.
  move=> G0 xae.
  rewrite ltr_norml; apply/andP; split.
    move: xae; rewrite in_itv/= => /andP[_].
    by rewrite ltrBrDl ltrBlDl addrC.
  move: xae; rewrite in_itv/= => /andP[+ _].
  rewrite -subr_lt0 => /lt_le_trans; apply.
  exact: ltW.
apply.
- move=> x xae; apply: fdf.
  rewrite inE; apply: aeU => /=; apply: H => //.
  by move: x xae; apply: subset_itvl; rewrite bnd_simp lerD2l ge_min lexx.
- move=> x xae; apply: gdg.
  rewrite inE; apply: aeU => /=; apply: H => //.
  by move: x xae; apply: subset_itvl; rewrite bnd_simp lerD2l ge_min lexx.
- rewrite -fa0; apply: cvg_at_right_filter.
  suff : {for a, continuous f} by [].
  apply/differentiable_continuous/derivable1_diffP.
  apply: ex_derive; apply: fdf.
  rewrite inE.
  by case: Ua => r /= r0; apply; rewrite /= subrr normr0.
- rewrite -ga0.
  apply: cvg_at_right_filter.
  suff : {for a, continuous g} by [].
  apply/differentiable_continuous/derivable1_diffP.
  apply: ex_derive; apply: gdg.
  rewrite inE.
  by case: Ua => r /= r0; apply; rewrite /= subrr normr0.
- move=> x xae; apply: cdg' => /=.
    apply: H => //.
    by move: x xae; apply: subset_itvl; rewrite bnd_simp lerD2l ge_min lexx orbT.
  rewrite gt_eqF//.
  by move: xae; rewrite in_itv/= => /andP[].
Qed.

End lhopital0.

Section lhopital1.
Context {R : realType}.
Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U).
Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x))
           (gdg : forall x, x \in U -> is_derive x 1 g (dg x)).
Hypotheses (fa0 : f a = 0) (ga0 : g a = 0)
           (cdg : \forall x \near a^', dg x != 0).

Lemma lhopital_left (l : R) :
  df x / dg x @[x --> a^'-] --> l -> f x / g x @[x --> a^'-] --> l.
Proof.
move=> fgbl; apply/cvg_at_leftNP.
set h := (X in X x @[x --> _]).
rewrite (_ : h = (fun x => (fun y => (f \o -%R) y / (g \o -%R) y) x))//.
have := @lhopital_right R (f \o -%R) (fun x => (df (- x)) * -1)
  (g \o -%R) (fun x => (dg (- x)) * -1) (- a) (-%R @` U).
apply.
- by rewrite nbhsNimage/=; exists U.
- move=> x; rewrite inE/= => -[r Ur] <-{x}.
  rewrite opprK; apply: is_derive1_comp.
  by rewrite opprK; apply: fdf; exact: mem_set.
- move=> x; rewrite inE/= => -[r Ur] <-{x}.
  rewrite opprK; apply: is_derive1_comp.
  by rewrite opprK; apply: gdg; exact: mem_set.
- by rewrite /= opprK.
- by rewrite /= opprK.
- case: cdg => e/= e0 H; near=> x.
  rewrite mulrN1 oppr_eq0.
  apply: H => /=.
    rewrite -normrN opprB addrC.
    by near: x; exists e.
  rewrite eqr_oppLR.
  by near: x; exact: nbhs_dnbhs_neq.
- apply/cvg_at_rightNP.
  rewrite opprK/=; apply: cvg_trans fgbl.
  apply: near_eq_cvg; near=> x.
  by rewrite /= opprK !mulrN1 mulNr invrN mulrN opprK.
Unshelve. all: by end_near. Qed.

End lhopital1.