exact Nat.not_le_of_lt hlt hinv
case h
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv : ↑k > i
hik : ¬i = ↑k
⊢ False
no goals