rw [dvd_iff_mod_eq_zero]
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ ↑p ∣ -[a✝+1]
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : natAbs -[a✝+1] % p = 0
⊢ mod -[a✝+1] ↑p = 0