have : Even (n - 1 + 1) := Nat.even_succ_of_odd this
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this : Odd (n - 1)
⊢ False
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even (n - 1 + 1)
⊢ False