calc i₁.1 + m * j₁.1
  _ < m + m * j₁.1 := Nat.add_lt_add_right i₁.2 _
  _ = m * (j₁.1 + 1) := by rewrite [Nat.add_comm m]; rfl
  _ ≤ m * j₂.1 := Nat.mul_le_mul_left m h
  _ ≤ i₂.1 + m * j₂.1 := Nat.le_add_left ..
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ rlexProd i₁ j₁ < rlexProd i₂ j₂
no goals