refine Or.imp_right ?_ <| ivs'_lt iv hmem
case right.inl
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'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
hmem : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
case right.inl
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'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
hmem : iv ∈ ivs'
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1