simp only [← ZMod.intCast_eq_intCast_iff, Int.cast_neg] at hbc hab
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
⊢ ↑p ∣ c
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c