no goals
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ Int.gcd a ↑p ≠ 1
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]