intro h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ n - ↑k - 1 ≤ ↑j → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }