α : Type u
l : List α
n : ℕ
⊢ n ≤ length l → rotate' l n = drop n l ++ take n l
α : Type u
l : List α
n : ℕ
⊢ n ≤ length l → rotate l n = drop n l ++ take n l
rw [rotate_eq_rotate']
no goals
α : Type u
l : List α
n : ℕ
⊢ n ≤ length l → rotate' l n = drop n l ++ take n l
exact rotate'_eq_drop_append_take