Theorem: Stream'.sum_succ (ListPowersProblem/StreamLemmas.lean)

State before:
α : Type ?u.12759
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ (i + 1) = sum σ i + σ (i + 1)
Tactic:
simp [sum, take_succ_to_concat, Nat.add_assoc]
State after:
no goals