ext n
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
⊢ shift (cumsum u) = cumsum u + u
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ shift (cumsum u) n = (cumsum u + u) n