proposition: Lemma sumn_range (k1 k2 : nat) (c : nat -> nat): k1 <= k2 -> (forall i j, i <= j < (k2 - k1).+1 -> c (j + k1) <= c (i + k1)) -> \sum_(k1 <= i < k2) (c i - c i.+1) = c k1 - c k2.
proof: Proof. rewrite leq_eqVlt => /predU1P[<- h|]; first by rewrite big_geq // subnn. rewrite -subn_gt0=> gt0_k2Bk1 h; rewrite -{1}[k1]add0n big_addn. case k1Bk2E: (k2 - k1) gt0_k2Bk1 h => [|n] // _ h. rewrite big_nat sumnB -?big_nat; last first. move=> i /andP[_]; rewrite ltnS -addSn => le_in. by apply/h; rewrite leqnSn /= !ltnS. rewrite big_nat_recl ?big_nat_recr //= subnDA addnK. rewrite add0n -addSn -k1Bk2E subnK // leqNgt; apply/negP. by move/ltnW; rewrite -subn_eq0 k1Bk2E. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)