split_ifs with hx
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
⊢ x ^ (p - 1) = if x ≠ 0 then 1 else 0
case pos
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : x ≠ 0
⊢ x ^ (p - 1) = 1

case neg
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : ¬x ≠ 0
⊢ x ^ (p - 1) = 0