[Merged by Bors] - chore(analysis/normed_space/basic): introduce `norm_smul_le` #18650

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.