conv => rhs; change (m+1)*n + m; rw [Nat.add_comm _ m]
case refl
m n : Nat
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ ↑i + k + 1 + (m + 1) * n < (m + 1) * (n + 1) - 1
case refl
m n : Nat
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ ↑i + k + 1 + (m + 1) * n < m + (m + 1) * n