case zero
h : 0 < zero
⊢ ↑(zero - 1) = ↑zero - 1

case succ
n✝ : ℕ
h : 0 < Nat.succ n✝
⊢ ↑(Nat.succ n✝ - 1) = ↑(Nat.succ n✝) - 1
n : ℕ
h : 0 < n
⊢ ↑(n - 1) = ↑n - 1
cases n
case succ
n✝ : ℕ
h : 0 < Nat.succ n✝
⊢ ↑(Nat.succ n✝ - 1) = ↑(Nat.succ n✝) - 1
case zero
h : 0 < zero
⊢ ↑(zero - 1) = ↑zero - 1

case succ
n✝ : ℕ
h : 0 < Nat.succ n✝
⊢ ↑(Nat.succ n✝ - 1) = ↑(Nat.succ n✝) - 1
cases h
no goals
case succ
n✝ : ℕ
h : 0 < Nat.succ n✝
⊢ ↑(Nat.succ n✝ - 1) = ↑(Nat.succ n✝) - 1
simp