Wilson's theorem

import Mathlib

theorem wilson (p : ℕ) (hp : p.Prime) : (Nat.factorial (p - 1)) % p = p - 1 :=by
  have h_neg : (-1 : ZMod p).val = p - 1 := by
    have h_p : p = (p - 1) + 1 := (Nat.sub_add_cancel hp.pos).symm
    rw [h_p]
    exact ZMod.val_neg_one (p - 1)
  haveI : Fact p.Prime := ⟨hp⟩
  have h := ZMod.wilsons_lemma p
  have h_val := congr_arg ZMod.val h
  rw [ZMod.val_natCast] at h_val
  rw [h_neg] at h_val
  exact h_val