p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ natAbs k ^ 2
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ natAbs k
apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp
no goals
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ natAbs k ^ 2
rwa [sq, ← natAbs_mul, ← coe_nat_dvd_left, ← sq]