rw [not_iff_not]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : 1 < p
⊢ natAbs k % p ≠ 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