apply Nat.le_antisymm ?_ h
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j = n - ↑k - 1
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j ≤ n - ↑k - 1