`nbhsx_ballx` : `{posnum R}` or `R`?

[affeldt-aist]

analysis/theories/topology.v

Line 5062 in 81fec2f

Lemma nbhsx_ballx (x : M) (eps : {posnum R}) : nbhs x (ball x eps%:num).

wouldn't it be slightly more practical to have e of type R instead of {posnum R}?

[affeldt-aist]

See PR #1132 for the difference.