case mk
n m val✝ : ℕ
isLt✝ : val✝ < n + 1
h : { val := val✝, isLt := isLt✝ } ≠ 0
⊢ ↑(pred { val := val✝, isLt := isLt✝ } h) = ↑{ val := val✝, isLt := isLt✝ } - 1
n m : ℕ
j : Fin (n + 1)
h : j ≠ 0
⊢ ↑(pred j h) = ↑j - 1
cases j
no goals
case mk
n m val✝ : ℕ
isLt✝ : val✝ < n + 1
h : { val := val✝, isLt := isLt✝ } ≠ 0
⊢ ↑(pred { val := val✝, isLt := isLt✝ } h) = ↑{ val := val✝, isLt := isLt✝ } - 1
rfl