by_cases n = 0
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ (if n = 0 then 1 else n + 1) = n + 1
case pos
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h✝ : n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1

case neg
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h✝ : ¬n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1