case ofNat
a✝ : ℕ
⊢ ↑(Int.natAbs (Int.ofNat a✝)) = ↑(Int.ofNat a✝)

case negSucc
a✝ : ℕ
⊢ ↑(Int.natAbs (Int.negSucc a✝)) = ↑(Int.negSucc a✝)
a : ℤ
⊢ ↑(Int.natAbs a) = ↑a
cases a
no goals
case ofNat
a✝ : ℕ
⊢ ↑(Int.natAbs (Int.ofNat a✝)) = ↑(Int.ofNat a✝)
simp only [Int.natAbs_ofNat, Int.cast_ofNat, Int.ofNat_eq_coe]
no goals
case negSucc
a✝ : ℕ
⊢ ↑(Int.natAbs (Int.negSucc a✝)) = ↑(Int.negSucc a✝)
simp only [neg_eq_self_mod_two, Nat.cast_succ, Int.natAbs, Int.cast_negSucc]