a : Int
h : 0 ≤ a
n : Nat
e : a = ↑n
⊢ a = ↑(natAbs a)
a : Int
h : 0 ≤ a
⊢ a = ↑(natAbs a)
let ⟨n, e⟩ := eq_ofNat_of_zero_le h
a : Int
h : 0 ≤ a
n : Nat
e : a = ↑n
⊢ ↑n = ↑(natAbs ↑n)
a : Int
h : 0 ≤ a
n : Nat
e : a = ↑n
⊢ a = ↑(natAbs a)
rw [e]
no goals
a : Int
h : 0 ≤ a
n : Nat
e : a = ↑n
⊢ ↑n = ↑(natAbs ↑n)
rfl