feat(analysis/normed_space): nnreal.coe_nat_abs (#7911)

from LTE

src/analysis/normed_space/basic.lean

@@ -1223,6 +1223,12 @@ instance : normed_comm_ring ℤ :=
 
 @[norm_cast] lemma int.norm_cast_real (m : ℤ) : ∥(m : ℝ)∥ = ∥m∥ := rfl
 
+lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = nnnorm n :=
+nnreal.eq $ calc ((n.nat_abs : ℝ≥0) : ℝ)
+               = (n.nat_abs : ℤ) : by simp only [int.cast_coe_nat, nnreal.coe_nat_cast]
+           ... = abs n           : by simp only [← int.abs_eq_nat_abs, int.cast_abs]
+           ... = ∥n∥              : rfl
+
 instance : norm_one_class ℤ :=
 ⟨by simp [← int.norm_cast_real]⟩