no goals
α : Type u
a : α
l : List α
m : ℕ
⊢ rotate' (rotate' (a :: l) 0) m = rotate' (a :: l) (0 + m)
simp
no goals
α : Type u
n m : ℕ
⊢ rotate' (rotate' [] n) m = rotate' [] (n + m)
simp
no goals
α : Type u
a : α
l : List α
n m : ℕ
⊢ rotate' (rotate' (a :: l) (n + 1)) m = rotate' (a :: l) (n + 1 + m)
rw [rotate'_cons_succ, rotate'_rotate' _ n, add_right_comm, ← rotate'_cons_succ]