norm_num at this
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
this : 2 = 1 ∨ 2 = -1
⊢ False
no goals