feat(analysis): lemmas about nnnorm and nndist (#13498)
Most of these lemmas follow trivially from the `norm` versions. This is far from exhaustive.
Additionally:
* `nnreal.coe_supr` and `nnreal.coe_infi` are added
* The old `is_primitive_root.nnnorm_eq_one` is renamed to `is_primitive_root.norm'_eq_one` as it was not about `nnnorm` at all. The unprimed name is already taken in reference to `algebra.norm`.
* `parallelogram_law_with_norm_real` is removed since it's syntactically identical to `parallelogram_law_with_norm ℝ` and also not used anywhere.
