apply Nat.le_iff_lt_or_eq.mpr
case a
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
ivs' : Array (Inversion x)
hivs'✝ :
  Nat.fold' k
      (fun i ivs =>
        if h : x[↑i] > x[k] then
          Array.push ivs
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
              lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
        else ivs)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
hivs' : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd ≤ k
case a
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
ivs' : Array (Inversion x)
hivs'✝ :
  Nat.fold' k
      (fun i ivs =>
        if h : x[↑i] > x[k] then
          Array.push ivs
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
              lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
        else ivs)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
hivs' : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k