no goals
n m : ℕ
x : Fin n
y : Fin (n + 1)
h : ↑castSucc x < y
h' : optParam (↑(↑(succAbove y) x) < n) (_ : ↑(↑(succAbove y) x) < n)
⊢ castLT (↑(succAbove y) x) h' = x
simp only [succAbove_below _ _ h, castLT_castSucc]