rw [hab, hbc, ← sub_eq_zero, ← sub_eq_add_neg, ← Int.cast_neg, ← Int.cast_sub,
  ← Int.cast_sub] at h
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
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑(-c - c - c) = 0
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c