Alternating sums over integer intervals

This file gives a telescoping formula for alternating sums of consecutive pairs in an additive commutative group.

@[simp]

theorem TauCeti.sum_Icc_negOnePow_smul_add {G : Type u_1} [AddCommGroup G] (f : ℤ → G) (a b : ℤ) (hab : a ≤ b) : ∑ n ∈ Finset.Icc a b, (↑n.negOnePow • f n + ↑n.negOnePow • f (n + 1)) = ↑a.negOnePow • f a + ↑b.negOnePow • f (b + 1)

An alternating sum of consecutive pairs telescopes to its two end terms.