rewrite [Nat.not_lt] at hj
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ¬↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂