simp only [sum_succ, iterate, ← ih, add_right_inj]
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ sum σ (Nat.succ i) = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) (Nat.succ i)).fst
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = head (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).snd