simp
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ ↑(Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }) <
    (m + 1) * (n + 1) - 1
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < (m + 1) * (n + 1) - 1