. cases k
  . rwa [ofNat_eq_coe, dvd_iff_mod_eq_zero, ← Int.natAbs_eq_zero]
  .
    rw [dvd_iff_mod_eq_zero]
    rw [mod]
    simp at *
    rw [dvd_iff_mod_eq_zero]
    norm_cast
    rw [Nat.succ_eq_add_one] at a
    exact Iff.mp natAbs_eq_zero a
case mp
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : natAbs k % p = 0
⊢ ↑p ∣ k

case mpr
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : ↑p ∣ k
⊢ natAbs k % p = 0
case mpr
R : Type u
inst : CommRing R
p : ℕ
k : ℤ
inst_1 : IsDomain R
hp : 1 < p
a : ↑p ∣ k
⊢ natAbs k % p = 0