no goals
α : Type ?u.267830
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
n : ℤ
k : ℕ
⊢ natAbs (n ^ k) = natAbs n ^ k
induction' k with k ih <;> [rfl; rw [pow_succ', Int.natAbs_mul, pow_succ', ih]]