rewrite [← Nat.add_assoc, Nat.add_comm i.1 k.1, Nat.add_assoc]
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑i + (↑k + 1) < m
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑k + (↑i + 1) < m