case a
n : ℤ
⊢ ↑↑(Int.natAbs n) = ↑(↑nnabs ↑n)
n : ℤ
⊢ ↑(Int.natAbs n) = ↑nnabs ↑n
ext
no goals
case a
n : ℤ
⊢ ↑↑(Int.natAbs n) = ↑(↑nnabs ↑n)
rw [NNReal.coe_nat_cast, Int.cast_natAbs, Real.coe_nnabs, Int.cast_abs]