generalize `cvg_nbhsP` in `realfun.v` to any metric space

[affeldt-aist]

For the record, comment from PR #1396 by @zstone1 :
"It would be nice to have this for any metric space (or indeed any first-countable space).
But it's fine to have the specialized version for now if it's useful.
We can always go back and generalize later"

[affeldt-aist]

depends on PR #1589