feat(analysis/normed_space/basic): add has_nnnorm (#7986)
We create here classes `has_nndist` and `has_nnnorm` that are variants of `has_dist` and `has_norm` taking values in `ℝ≥0`. Obvious instances are `pseudo_metric_space` and `semi_normed_group`.
These are not used that much in mathlib, but for example `has_nnnorm` is quite convenient for LTE.
