proposition: Lemma telescope_sumn_in n m f : n <= m -> (forall i, n <= i < m -> f i <= f i.+1) -> \sum_(n <= k < m) (f k.+1 - f k) = f m - f n.
proof: Proof. move=> nm fle; rewrite (telescope_big (fun i j => f j - f i)). by case: ltngtP nm => // ->; rewrite subnn. move=> k /andP[nk km]; rewrite /= addnBAC ?subnKC ?fle ?(ltnW nk)//. elim: k nk km => [//| k IHk /[!ltnS]/[1!leq_eqVlt]+ km]. move=> /predU1P[/[dup]nk -> | nk]; first by rewrite fle ?nk ?leqnn 1?ltnW. by rewrite (leq_trans (IHk _ _) (fle _ _))// ltnW// ltnW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)