case a
α : Type u
β : Type v
δ : Type w
n m : ℕ
s : Stream' α
n✝ : ℕ
⊢ nth (drop n (drop m s)) n✝ = nth (drop (n + m) s) n✝
α : Type u
β : Type v
δ : Type w
n m : ℕ
s : Stream' α
⊢ drop n (drop m s) = drop (n + m) s
ext
no goals
case a
α : Type u
β : Type v
δ : Type w
n m : ℕ
s : Stream' α
n✝ : ℕ
⊢ nth (drop n (drop m s)) n✝ = nth (drop (n + m) s) n✝
simp [Nat.add_assoc]