proposition: Lemma telescopez a b (f : int -> R) : a <= b -> \sum_(a <= k < b :> int) (f (k + 1) - f k) = f b - f a.
proof: Proof. rewrite -{2}[a]add0r big_addz => hab /=. case e: (b - a) => [bma | bma]; last by move: hab; rewrite -subr_ge0 e. rewrite eq_big_int_nat /=. transitivity (\sum_(0 <= i < bma) (f (Posz (i + 1)%N + a) - f (Posz i + a))). apply: congr_big_nat => // i _ ; by rewrite PoszD addrAC. by rewrite (telescope_nat (fun i => f (Posz i + a))%R) // add0r -e addrNK. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp