refine Fin.ne_of_val_ne (Nat.ne_of_gt ?_)
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n) =
      Board.pivot i j
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n))