no goals
n m : ℕ
x : Fin n
y : Fin (n + 1)
h : y ≤ ↑castSucc x
h' : optParam (↑(succAbove y) x ≠ 0) (_ : ↑(succAbove y) x ≠ 0)
⊢ pred (↑(succAbove y) x) h' = x
simp only [succAbove_above _ _ h, pred_succ]