no goals
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
⊢ ↑q ≠ 0
rwa [← Nat.cast_zero, Ne.def, eq_iff_modEq_nat, Nat.modEq_zero_iff_dvd, ←
  hp.1.coprime_iff_not_dvd, Nat.coprime_primes hp.1 hq.1]