apply ih m
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ False
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ y = 2 * m