apply even_contra_helper
n : Nat
h : Even (Nat.succ (n + n))
⊢ False
case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ Even ?n'

case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ ?n' = Nat.succ (?n + ?n)

case n'
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat

case n
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat