case a
x : ℝ
h : 0 ≤ x
⊢ ↑(↑nnabs x) = ↑(toNNReal x)
x : ℝ
h : 0 ≤ x
⊢ ↑nnabs x = toNNReal x
ext
no goals
case a
x : ℝ
h : 0 ≤ x
⊢ ↑(↑nnabs x) = ↑(toNNReal x)
rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]