Adding the infinite versions of lemmas such as cvg_at_rightP in realfun.v

[Yosuke-Ito-345]

I am trying to formalize the infinite versions of lemmas in Section cvgr_fun_cvg_seq in realfun.v.
Some candidates are as follows.

Lemma cvg_ninftyP (f : R -> R) (l : R) :
  f x @[x --> -oo] --> l <->
  (forall u : R^nat, (u n @[n --> \oo] --> -oo) -> f (u n) @[n --> \oo] --> l).

Lemma cvg_pinftyP (f : R -> R) (l : R) :
  f x @[x --> +oo] --> l <->
  (forall u : R^nat, (u n @[n --> \oo] --> +oo) -> f (u n) @[n --> \oo] --> l).

If anybody is trying the same thing, please let me know to avoid duplicate work.
Since I am new to MathComp-Analysis, any advice is welcome.