apply isCoprime_of_dvd _ _ (not_and_of_not_left _ hpnezero)
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ IsCoprime p q
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ ∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ p → ¬z ∣ q