n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑castSucc (castLT i (_ : ↑i < n + 1)) = i

case hnc
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ¬↑castSucc (last n) < i
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑castSucc (castPred i) = i
rw [castPred, predAbove, dif_neg]
no goals
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑castSucc (castLT i (_ : ↑i < n + 1)) = i
simp [Fin.eq_iff_veq]
no goals
case hnc
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ¬↑castSucc (last n) < i
exact h.not_le