a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ ↑(natAbs a) = ↑(natAbs b)
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ a * a = b * b
rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]
no goals
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ ↑(natAbs a) = ↑(natAbs b)
exact Int.coe_nat_inj'.symm