obtain ⟨n, hn⟩ := p_dvd_c_of_ab_of_anegc hpri hp3 h H habs
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
⊢ False
case pos.refine'_3.intro
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
n : ℤ
hn : c = ↑p * n
⊢ False