apply Fin.rlexProd_lt_iff.mpr
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)) <
    ↑(Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) })
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∨
    Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ Fin.castSucc i < Fin.last m