rintro rfl
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
⊢ q ≠ 0
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