apply Nat.le_sub_of_add_le
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j ≤ n - (↑k + 1)
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j + (↑k + 1) ≤ n