ring_nf at he
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : (2 * a + 1) ^ 2 + (b + b) ^ 2 = e + e
⊢ False
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = e * 2
⊢ False