no goals
α : Type u
l : List α
n : ℕ
⊢ rotate' l (n % length l) = rotate' (rotate' l (n % length l)) (length (rotate' l (n % length l)) * (n / length l))
rw [rotate'_length_mul]
no goals
α : Type u
l : List α
n : ℕ
⊢ rotate' (rotate' l (n % length l)) (length (rotate' l (n % length l)) * (n / length l)) = rotate' l n
rw [rotate'_rotate', length_rotate', Nat.mod_add_div]