cases n.mod_two_eq_zero_or_one
n : Nat
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
case inl
n : Nat
h✝ : n % 2 = 0
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1

case inr
n : Nat
h✝ : n % 2 = 1
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1