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