English
Reversing after rotation by n is the reverse of the rotation by the complementary amount: l.reverse.rotate n = l.rotate (|l| - n mod |l|).reverse.
Русский
Разворот после поворота на n равен развороту на дополнительный сдвиг, затем разворот: l.reverse.rotate n = l.rotate (|l| - n mod |l|).reverse.
LaTeX
$$$\\forall l\\in\\mathrm{List}\\alpha,\\forall n:\\mathbb{N}, \\ l.reverse.rotate n = (l.rotate (|l| - n \\% |l|)).reverse$$$
Lean4
theorem rotate_reverse (l : List α) (n : ℕ) : l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse :=
by
rw [← reverse_reverse l]
simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate, length_reverse]
rw [← length_reverse]
let k := n % l.reverse.length
rcases hk' : k with - | k'
· simp_all! [k, length_reverse, ← rotate_rotate]
· rcases l with - | ⟨x, l⟩
· simp
· rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
· exact Nat.sub_le _ _
· exact Nat.sub_lt (by simp) (by simp_all! [k])
