have ha : a ≠ 0 := fun ha => by simp [ha] at hprod
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
⊢ False
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
⊢ False