case h.h
n m : ℕ
x✝ : Fin n
⊢ ↑(↑(succAbove (last n)) x✝) = ↑(↑castSucc x✝)
n m : ℕ
⊢ succAbove (last n) = castSucc
ext
no goals
case h.h
n m : ℕ
x✝ : Fin n
⊢ ↑(↑(succAbove (last n)) x✝) = ↑(↑castSucc x✝)
simp only [succAbove_below, castSucc_lt_last]