[GOAL]
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ Int.gcd a ↑p ≠ 1
[PROOFSTEP]
rw [Ne, Int.gcd_comm, Int.gcd_eq_one_iff_coprime, (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd,
  Classical.not_not, int_cast_zmod_eq_zero_iff_dvd]
