Fermat's little theorem

import Mathlib

theorem fermat_little (p : ℕ) (hp : p.Prime) (a : ℤ) (h : ¬ (p : ℤ) ∣ a) : a ^ (p - 1) ≡ 1 [ZMOD p] := by
  have hpn : IsCoprime a (p : ℤ) := by
    rw [Int.isCoprime_iff_nat_coprime]
    simp
    rw [Nat.coprime_comm]
    rw [Nat.Prime.coprime_iff_not_dvd hp]
    rwa [← Int.ofNat_dvd_left]
  exact Int.ModEq.pow_card_sub_one_eq_one hp hpn