Theorem: sum_n (ListPowersProblem.lean)

State before:
n j : ℕ
inst✝ : NeZero n
⊢ sum (fun i => i + i / (n + 1) + 1) (j + j / n) = 3 * (j ^ 2 + j) + 1
Tactic:
sorry
State after:
no goals