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