dsimp [Board.pathT, Board.pivot]
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathT i j
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j) ∈
      List.ofFn fun x => Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j)