cases x <;> cases n <;> simp_all <;> simp_arith at *
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
case succSucc.succ.succ
n' n✝¹ : Nat
hx : Even (Nat.succ n✝¹)
n✝ : Nat
ih : ∀ (n : Nat), ¬n✝¹ = 2 * n
hn : n✝¹ = 2 * n✝
⊢ False