intro x y hcoprime hx hy
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
⊢ ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
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 : Even x
hy : Even y
⊢ False