don't we need `cvg_dnbhs_at_right`?

[affeldt-aist]

Lemma cvg_dnbhs_at_right (f : R -> R) (p : R) (l : R) :
  f x @[x --> p^'] --> l ->
  f x @[x --> p^'+] --> l.
Proof.
apply: cvg_trans; apply: cvg_app.
by apply: within_subset => r ?; rewrite gt_eqF.
Qed.

@agontard