rw [zero_sub, add_zero, Odd.neg_pow (by norm_num), ← sub_eq_add_neg, sub_eq_iff_eq_add] at h
a : ℤ
hapos : a ≠ 0
p : ℤ
hpnezero : p ≠ 0
hc : ¬Even (p + 0)
hb : ¬Even (0 - p)
h : a ^ 3 + (0 - p) ^ 3 = (p + 0) ^ 3
hbccoprime : IsCoprime (0 - p) (p + 0)
hp : p + 0 - (0 - p) = 2 * p
hq : p + 0 + (0 - p) = 2 * 0
⊢ False
a : ℤ
hapos : a ≠ 0
p : ℤ
hpnezero : p ≠ 0
hc : ¬Even (p + 0)
hb : ¬Even (0 - p)
h : a ^ 3 = p ^ 3 + p ^ 3
hbccoprime : IsCoprime (0 - p) (p + 0)
hp : p + 0 - (0 - p) = 2 * p
hq : p + 0 + (0 - p) = 2 * 0
⊢ False