induction' h : (a * b * c).natAbs using Nat.strong_induction_on with k' IH generalizing a b c
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
case h
k' : ℕ
IH : ∀ m < k', ∀ (a b c : ℤ), a ≠ 0 → b ≠ 0 → c ≠ 0 → (a * b * c).natAbs = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : (a * b * c).natAbs = k'
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3