Theta Jacobian

Pure telescoping input for the theta Jacobian calculation. The index k is the unit-step number, so the coefficient k+1 matches the path coordinate of the interior vertex represented by that step.

theorem Bananas.weighted_step_difference_telescope (A : ℕ) (s : ℕ → ℤ) : ∑ k ∈ Finset.range (A - 1), ↑(k + 1) * (s (k + 1) - s k) - ↑A * s (A - 1) = -∑ k ∈ Finset.range A, s k