proposition: Lemma telescope_sumn n m f : {homo f : x y / x <= y} -> \sum_(n <= k < m) (f k.+1 - f k) = f m - f n.
proof: Proof. move=> fle; case: (ltnP n m) => nm. by apply: (telescope_sumn_in (ltnW nm)) => ? ?; apply: fle. by apply/esym/eqP; rewrite big_geq// subn_eq0 fle. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)