chore(analysis/normed_space/basic): introduce `norm_smul_le`
Currently `norm_smul_le x y` is just a special case of `(norm_smul x y).le`; but if in future we generalize `normed_space` to work over normed rings, it will continue to hold where `norm_smul` no longer does.
This adjusts downstream proofs to use the weaker lemma too when the stronger one isn't needed.
This adds the corresponding `nnnorm` and `dist` and `nndist` lemmas too.
