simp only [drop, nth]
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ take i σ ++ take j (drop i σ) = take (i + j) σ
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ