refine Nat.mul_le_mul_left (m+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 })))
⊢ (m + 1) * (↑j + k + 1) ≤ (m + 1) * n
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 })))
⊢ ↑j + k + 1 ≤ n