English
For xs with Nodup, and n with n+1 < length(xs), formPerm xs xs[n] = xs[n+1].
Русский
Для нескомпонов l без повторов, при n+1 < длины l, formPerm xs xs[n] = xs[n+1].
LaTeX
$$$\forall \alpha\, [\DecidableEq\ \alpha],\forall xs:\,\mathrm{List}\ \alpha,\ xs.Nodup\rightarrow\forall n:\,\mathrm{Nat},\hn: n+1 < xs.length,\ formPerm\ xs\ xs[n] = xs[n+1]$$$
Lean4
theorem formPerm_apply_lt_getElem (xs : List α) (h : Nodup xs) (n : ℕ) (hn : n + 1 < xs.length) :
formPerm xs xs[n] = xs[n + 1] := by
induction n generalizing xs with
| zero => simpa using formPerm_apply_getElem_zero _ h _
| succ n IH =>
rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
· simp at hn
· rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]
· specialize IH (y :: l) h.of_cons _
· simpa [Nat.succ_lt_succ_iff] using hn
simp only [swap_apply_eq_iff, coe_mul, formPerm_cons_cons, Function.comp]
simp only [getElem_cons_succ] at *
rw [← IH, swap_apply_of_ne_of_ne] <;>
· intro hx
rw [← hx, IH] at h
simp [getElem_mem] at h
