no goals
α : Type u
l : List α
n : ℕ
h : length l = 0
⊢ rotate l n = rotate' l n
simp_all [length_eq_zero]
α : Type u
l : List α
n : ℕ
h : ¬length l = 0
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
α : Type u
l : List α
n : ℕ
h : ¬length l = 0
⊢ rotate l n = rotate' l n
rw [← rotate'_mod,
    rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
no goals
α : Type u
l : List α
n : ℕ
h : ¬length l = 0
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
simp [rotate]