English
For any l, n and k a finite index in l.rotate n, the value (l.rotate n).get k equals l.get at the index (k.val + n) mod length(l).
Русский
Для любого l, n и k из финитного множества индексов l.rotate n, значение (l.rotate n).get k равно l.get по индексу (k.значение + n) mod длина(l).
LaTeX
$$$\\forall {\alpha} (l:\\mathrm{List}\\alpha) (n:\\mathbb{N}) (k:\\mathrm{Fin}(|l\\rotate n|)), \\ (l\\rotate n).get k = l.get \\langle (k.1 + n) \\% |l|, \\rangle$$$
Lean4
theorem get_rotate (l : List α) (n : ℕ) (k : Fin (l.rotate n).length) :
(l.rotate n).get k = l.get ⟨(k + n) % l.length, mod_lt _ (length_rotate l n ▸ k.pos)⟩ := by simp [getElem_rotate]
