rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑p ∣ c
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑c = 0