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

State before:
α : Type ?u.12375
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ (i + 1) = head σ + sum (tail σ) i
Tactic:
simp only [sum, take, head, nth, Nat.add_eq, add_zero, Nat.sum_cons]
State after:
no goals