intro k
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (m - ↑i - 1)),
    ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i x)) (_ : ↑(Fin.succ (Fin.eadd i x)) < m + 1)) (Fin.last n) =
        Board.pivot i j
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