. simp only [List.length_pmap, beq_eq_false_iff_ne, ne_eq]
  dsimp [Board.path, Board.pathL, Board.pathB, Board.pathR, Board.pathT]
  simp only [List.length_append, List.length_ofFn]
  rewrite [Nat.add_assoc (n-j.1 + (m-i.1-1)), ← Nat.mul_two, Nat.mul_mod_left]
  decide
m n : Nat
i : Fin m
j : Fin n
⊢ (List.length
          (List.pmap Fin.restrict (Board.path i j)
            (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)) %
        2 ==
      1) =
    false

m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ∈
      List.pmap Fin.restrict (Board.path i j)
        (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ∈
      List.pmap Fin.restrict (Board.path i j)
        (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)