dsimp [Board.path]
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.path i j
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ++ Board.pathB n i ++ Board.pathR m j ++ Board.pathT i j