dsimp [inversions]
n : Nat
x : Permutation n
⊢ Array.Nodup (inversions x) ∧ ∀ (iv : Inversion x), iv ∈ inversions x → ↑iv.snd < n
n : Nat
x : Permutation n
⊢ Array.Nodup
      (Nat.fold' n
        (fun j =>
          Nat.fold' ↑j fun i ivs =>
            if h : x[↑i] > x[↑j] then
              Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
            else ivs)
        #[]) ∧
    ∀ (iv : Inversion x),
      iv ∈
          Nat.fold' n
            (fun j =>
              Nat.fold' ↑j fun i ivs =>
                if h : x[↑i] > x[↑j] then
                  Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
                else ivs)
            #[] →
        ↑iv.snd < n