exact And.imp_right Nat.le.step
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]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1
no goals