simp only [Fin.lt_def]
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ { val := ↑i₁ + m * ↑j₁, isLt := (_ : ↑i₁ + m * ↑j₁ < m * n) } <
      { val := ↑i₂ + m * ↑j₂, isLt := (_ : ↑i₂ + m * ↑j₂ < m * n) } ↔
    j₁ < j₂ ∨ j₁ = j₂ ∧ i₁ < i₂
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂