exact Fin.rlexProd_lt_of_snd _ _ j.2
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n))
no goals