intro hj
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ↑j < 0 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ #[]
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
hj : ↑j < 0
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ #[]