exact Nat.lt_irrefl k
case left.refine_1
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
      lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
      inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k < k → False
no goals