English
For any l and n with n less than length of cyclicPermutations l, the nth element equals l.rotate n.
Русский
Для любого списка l и натурального n, меньшего длины cyclicPermutations(l), элемент под индексом n равен l.rotate n.
LaTeX
$$$ \forall {\alpha} (l: List(\alpha)) (n: \mathbb{N}) (h: n < \text{length}(\text{cyclicPermutations}~l)), \\ (\text{cyclicPermutations}~l)[n] = l.rotate~n $$$
Lean4
@[simp]
theorem getElem_cyclicPermutations (l : List α) (n : Nat) (h : n < length (cyclicPermutations l)) :
(cyclicPermutations l)[n] = l.rotate n := by
cases l with
| nil => simp
| cons a
l =>
simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails, getElem_inits]
rw [rotate_eq_drop_append_take (by simpa using h.le)]
