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 : Nat.succ a✝ % p = 0
⊢ ↑p ∣ ↑a✝ + 1
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : Nat.succ a✝ % p = 0
⊢ mod (↑a✝ + 1) ↑p = 0