cases n
m n : Nat
hn : n > 0
⊢ m + pred n = pred (m + n)
case zero
m : Nat
hn : zero > 0
⊢ m + pred zero = pred (m + zero)

case succ
m n✝ : Nat
hn : succ n✝ > 0
⊢ m + pred (succ n✝) = pred (m + succ n✝)