refine Nat.fold'_induction (motive := fun l (ivs' : Array (Inversion x)) => ivs'.Nodup ∧ ∀ iv, iv ∈ ivs' → iv.snd.1 < k ∨ (iv.snd.1 = k ∧ iv.fst.1 < l)) k _ ivs ?_ ?_
case refine_2.refl
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
⊢ Array.Nodup
      (Nat.fold' k
        (fun i ivs =>
          if h : x[↑i] > x[k] then
            Array.push ivs
              { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
                lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
          else ivs)
        ivs) ∧
    ∀ (iv : Inversion x),
      iv ∈
          Nat.fold' k
            (fun i ivs =>
              if h : x[↑i] > x[k] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
                    lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
              else ivs)
            ivs →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
case refine_2.refl.refine_1
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
⊢ (fun l ivs' => Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l) 0 ivs

case refine_2.refl.refine_2
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
⊢ ∀ (i : Nat) (hi : i < k) (a : Array (Inversion x)),
    (fun l ivs' => Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l) i a →
      (fun l ivs' => Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l)
        (i + 1)
        (if h : x[↑{ val := i, isLt := hi }] > x[k] then
          Array.push a
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) { val := i, isLt := hi },
              snd := { val := k, isLt := hk }, lt := (_ : ↑{ val := i, isLt := hi } < ↑{ val := k, isLt := hk }),
              inverted := h }
        else a)