Lean4
/-- Shrink a permutation of a list, slicing a segment in the middle.
The sizes of the slice being removed start at `n` (with `n` the length
of the list) and then `n / 2`, then `n / 4`, etc. down to 1. The slices
will be taken at index `0`, `n / k`, `2n / k`, `3n / k`, etc.
-/
protected def shrinkPerm {α : Type} [DecidableEq α] :
(Σ' xs ys : List α, xs ~ ys ∧ ys.Nodup) → List (Σ' xs ys : List α, xs ~ ys ∧ ys.Nodup)
| xs => do
let k := xs.1.length
let n ← (sliceSizes k).force
let i ← List.finRange <| k / n
pure <| Perm.slice (i * n) n xs