cases Nat.eq_or_lt_of_le hj with
| inl heq =>
  cases Fin.eq_of_val_eq heq
  simp only [true_and]
  exact Nat.add_lt_add_iff_right _ i₁.1 i₂.1
| inr hlt =>
  have : j₁ ≠ j₂ := fun h =>
    Nat.lt_irrefl _ (h ▸ hlt)
  simp only [this, false_and, iff_false, Nat.not_lt]
  apply Nat.le_of_lt
  exact rlexProd_lt_of_snd i₂ i₁ hlt
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
no goals