n✝ m n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ ↑(succAbove (succ i)) (succ 0) = succ (↑(succAbove i) 0)
n✝ m n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ ↑(succAbove (succ i)) 1 = succ (↑(succAbove i) 0)
rw [← succ_zero_eq_one]
no goals
n✝ m n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ ↑(succAbove (succ i)) (succ 0) = succ (↑(succAbove i) 0)
exact succ_succAbove_succ i 0