dsimp [Board.path, Board.pathL, Board.pathB, Board.pathR, Board.pathT]
m n : Nat
i : Fin m
j : Fin n
⊢ ¬List.length (Board.path i j) % 2 = 1
m n : Nat
i : Fin m
j : Fin n
⊢ ¬List.length
          ((((List.ofFn fun k =>
                  Fin.rlexProd (Fin.castSucc i)
                    (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k)))) ++
                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)) ++
              List.ofFn fun x => Fin.rlexProd (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) }) ++
            List.ofFn fun x => Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j)) %
        2 =
      1