English
Reversing after rotating equals rotating the reversed by a complementary amount: (l.rotate n).reverse = l.reverse.rotate (|l| - n mod |l|).
Русский
Обращение после поворота эквивалентно повороту обращённого на дополнительный смещение: (l.rotate n).reverse = l.reverse.rotate (длина(l) - n mod длина(l)).
LaTeX
$$$\\forall l\\in\\mathrm{List}\\alpha,\\forall n:\\mathbb{N}, \\ (l.rotate n).reverse = l.reverse.rotate (|l| - n \\% |l|)$$$
Lean4
theorem reverse_rotate (l : List α) (n : ℕ) : (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length) :=
by
rw [← length_reverse, ← rotate_eq_iff]
induction n generalizing l with
| zero => simp
| succ n hn =>
rcases l with - | ⟨hd, tl⟩
· simp
· rw [rotate_cons_succ, ← rotate_rotate, hn]
simp
