. exact lt_last_of_mem_pathB n i a hB
case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1