English
For Nodup l and n∈Nat, the value of (formPerm l)^n on l[i] equals l[(i+n) mod length(l)], with the appropriate modulo.
Русский
Для Nodup l и n∈Nat, значение (formPerm l)^n на l[i] равно l[(i+n) mod длина(l)], с допустимым остатком.
LaTeX
$$$\forall {\alpha:[DecidableEq\alpha]}\,(l:\,\mathrm{List}\ \alpha),\ l.Nodup\rightarrow\forall (n:\,\mathrm{Nat}) (i:\,\mathrm{Nat}) (h:\, i < l.length),\ (formPerm\ l\^ n)\ l[i] = l[(i+n) \% l.length]'(\\mathrm{Nat.mod\\_lt} _ (i.0\\le).trans(h))$$$
Lean4
theorem formPerm_reverse : ∀ l : List α, formPerm l.reverse = (formPerm l)⁻¹
| [] => rfl
| [_] => rfl
| a :: b :: l => by simp [formPerm_append_pair, swap_comm, ← formPerm_reverse (b :: l)]
