rw [pow_add, pow_one]
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1 + 1) ≡ n [ZMOD ↑p]
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) * n ≡ n [ZMOD ↑p]