intro k
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (m - ↑i - 1)),
    ¬Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j) =
        Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ¬Fin.rlexProd { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) } (Fin.castSucc j) =
      Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)