rw [nat_valuation_eq_zero_iff hp]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ nat_valuation p (natAbs k) = 0 ↔ k % ↑p ≠ 0
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ natAbs k % p ≠ 0 ↔ k % ↑p ≠ 0