intro n hn
case succSucc
n' x : Nat
hx : Even x
ih : ∀ (n : Nat), x ≠ Nat.succ (n + n)
⊢ ∀ (n : Nat), Nat.succ (Nat.succ x) ≠ Nat.succ (n + n)
case succSucc
n' x : Nat
hx : Even x
ih : ∀ (n : Nat), x ≠ Nat.succ (n + n)
n : Nat
hn : Nat.succ (Nat.succ x) = Nat.succ (n + n)
⊢ False