English
For Nodup xs and i with i < length xs, formPerm xs xs[i] equals the next element xs[(i+1) mod length xs].
Русский
Для Nodup xs и i < length(xs) выполняется: formPerm xs xs[i] = xs[(i+1) mod length xs].
LaTeX
$$$\forall \alpha\, [\DecidableEq\ \alpha],\forall xs:\,\mathrm{List}\ \alpha,\ xs.Nodup\rightarrow\forall i:\,\mathrm{Nat},\ h:\, i < xs.length,\ formPerm xs xs[i] = xs[(i+1) \% xs.length]$$$
Lean4
theorem formPerm_apply_getElem (xs : List α) (w : Nodup xs) (i : ℕ) (h : i < xs.length) :
formPerm xs xs[i] = xs[(i + 1) % xs.length]'(Nat.mod_lt _ (i.zero_le.trans_lt h)) :=
by
rcases xs with - | ⟨x, xs⟩
· simp at h
· have : i ≤ xs.length := by
refine Nat.le_of_lt_succ ?_
simpa using h
rcases this.eq_or_lt with (rfl | hn')
· simp
· rw [formPerm_apply_lt_getElem (x :: xs) w _ (Nat.succ_lt_succ hn')]
congr
rw [Nat.mod_eq_of_lt]; simpa [Nat.succ_eq_add_one]
