ring
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
⊢ p + q + b - (p + q - b) = 2 * b
no goals