use (1 + 2 * a + 2 * a ^ 2 + 2 * b + 2 * b ^ 2)
case intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ ∃ r, 2 + a * 4 + a ^ 2 * 4 + b * 4 + b ^ 2 * 4 = r * 2
case h
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ 2 + a * 4 + a ^ 2 * 4 + b * 4 + b ^ 2 * 4 = (1 + 2 * a + 2 * a ^ 2 + 2 * b + 2 * b ^ 2) * 2