induction' a using Nat.strongInductionOn with a ih
a b c : ℕ
ha : 0 < a
hb : 0 < b
hc : 0 < c
h : a ^ 4 = b ^ 4 + c ^ 2
⊢ False
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
⊢ False