conv at ha =>
  dsimp [Board.path]
  simp only [List.mem_append, or_assoc]
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.path i j
⊢ ↑a < (m + 1) * (n + 1) - 1
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathL i j ∨ a ∈ Board.pathB n i ∨ a ∈ Board.pathR m j ∨ a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1