intro h
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
⊢ Even m → Even (Nat.succ (Nat.succ x) + m)
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (Nat.succ (Nat.succ x) + m)