proposition: Lemma sum0n_range (k : nat) (c : nat -> nat): (forall i j, i <= j < k.+1 -> c j <= c i) -> \sum_(0 <= i < k) (c i - c i.+1) = c 0 - c k.
proof: Proof. move=> h; apply/sumn_range; rewrite ?subn0=> // i j le. by rewrite !addn0; apply/h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)