have a_odd : Odd a := sorry
case ind.inl
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
hab : a.gcd b = 1
c_even : Even c
⊢ False
case ind.inl
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
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
⊢ False