proposition: Lemma telescope_sumr n m (f : nat -> V) : n <= m -> \sum_(n <= k < m) (f k.+1 - f k) = f m - f n.
proof: Proof. move=> nm; rewrite (telescope_big (fun i j => f j - f i)). by case: ltngtP nm => // ->; rewrite subrr. by move=> k /andP[nk km]/=; rewrite addrC subrKA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)