n✝ m n : ℕ
j : Fin n
this : ↑(succAbove (succ 0)) (succ j) = succ (↑(succAbove 0) j)
⊢ ↑(succAbove 1) (succ j) = succ (succ j)
n✝ m n : ℕ
j : Fin n
⊢ ↑(succAbove 1) (succ j) = succ (succ j)
have := succ_succAbove_succ 0 j
no goals
n✝ m n : ℕ
j : Fin n
this : ↑(succAbove (succ 0)) (succ j) = succ (↑(succAbove 0) j)
⊢ ↑(succAbove 1) (succ j) = succ (succ j)
rwa [succ_zero_eq_one, zero_succAbove] at this