case a
α : Type u
β : Type v
δ : Type w
i : ℕ
s : Stream' α
n✝ : ℕ
⊢ nth (tail (drop i s)) n✝ = nth (drop (i + 1) s) n✝
α : Type u
β : Type v
δ : Type w
i : ℕ
s : Stream' α
⊢ tail (drop i s) = drop (i + 1) s
ext
no goals
case a
α : Type u
β : Type v
δ : Type w
i : ℕ
s : Stream' α
n✝ : ℕ
⊢ nth (tail (drop i s)) n✝ = nth (drop (i + 1) s) n✝
simp [add_comm, add_assoc, add_left_comm]