proposition: Lemma telescope_sume n m (f : nat -> \bar R) : (forall i, (n <= i <= m)%N -> f i \is a fin_num) -> (n <= m)%N -> \sum_(n <= k < m) (f k.+1 - f k) = f m - f n.
proof: Proof. move=> nmf nm; under eq_big_nat => i /andP[ni im] do rewrite -[f i.+1]fineK -1?[f i]fineK ?(nmf, ni, im) 1?ltnW//= -EFinD. by rewrite sumEFin telescope_sumr// EFinB !fineK ?nmf ?nm ?leqnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed