n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ ↑castSucc 0 = 0

case h
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ ↑castSucc 0 < a
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ ↑(succAbove a) 0 = 0
rw [Fin.succAbove_below]
no goals
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ ↑castSucc 0 = 0
simp
case h
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ 0 < a
case h
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ ↑castSucc 0 < a
simp only [castSucc_zero]
no goals
case h
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ 0 < a
exact bot_lt_iff_ne_bot.mpr ha