let ⟨i,j,hlt,hinv⟩ := iv
n : Nat
x : Permutation n
iv : Inversion x
⊢ iv ∈ inversions x
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ inversions x