proposition: Lemma telescope_sumr_eq n m (f u : nat -> V) : n <= m -> (forall k, (n <= k < m)%N -> u k = f k.+1 - f k) -> \sum_(n <= k < m) u k = f m - f n.
proof: Proof. by move=> ? uE; under eq_big_nat do rewrite uE //=; exact: telescope_sumr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)