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