α : Type u
l : List α
⊢ drop (length l) l ++ take (length l) l = l
α : Type u
l : List α
⊢ rotate' l (length l) = l
rw [rotate'_eq_drop_append_take le_rfl]
no goals
α : Type u
l : List α
⊢ drop (length l) l ++ take (length l) l = l
simp