induction hn' with
| zero => simp_all
| succSucc x hx ih =>
  intro n hn
  cases x <;> cases n <;> simp_all <;> simp_arith at *
  case succSucc.succ.succ y m =>
    apply ih m
    assumption
n' : Nat
hn' : Even n'
⊢ ∀ (n : Nat), n' ≠ Nat.succ (n + n)
no goals