English
Remove a slice of length m at index n in a list and its permutation, obtaining a shorter pair that remains a permutation with the longer list still nodup.
Русский
Удалить участок длины m по индексу n в списке и соответствующую перестановку, чтобы получить более короткую пару, которая по-прежнему образует перестановку и у второй компоненты сохраняется свойство Nodup.
LaTeX
$$$\text{slice}(n,m) : (xs,ys, h, h') \mapsto (List.dropSlice n m xs, ys \cap xs', (xs' \sim ys.\mathrm{inter} xs'), ys'.\mathrm{Nodup})$$$
Lean4
/-- Remove a slice of length `m` at index `n` in a list and a permutation, maintaining the property
that it is a permutation.
-/
def slice [DecidableEq α] (n m : ℕ) : (Σ' xs ys : List α, xs ~ ys ∧ ys.Nodup) → Σ' xs ys : List α, xs ~ ys ∧ ys.Nodup
| ⟨xs, ys, h, h'⟩ =>
let xs' := List.dropSlice n m xs
have h₀ : xs' ~ ys.inter xs' := List.Perm.dropSlice_inter _ _ h h'
⟨xs', ys.inter xs', h₀, h'.inter _⟩
