apply Int.eq_of_mul_eq_mul_left two_ne_zero
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ q - p = b
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ 2 * (q - p) = 2 * b