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