dsimp [Board.pathB]
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathB n i
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈
      List.ofFn fun k =>
        Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n)