no goals
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ drop (List.length []) ([] ++ₛ s) = s
rfl
no goals
α : Type u
β : Type v
δ : Type w
a : α
l : List α
s : Stream' α
⊢ drop (List.length (a :: l)) (a :: l ++ₛ s) = s
rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]