proposition: Lemma sumn_wgt_range (k : nat) (c : nat -> nat): (forall i j, i <= j < k.+1 -> c j <= c i) -> \sum_(i < k) (c i - c i.+1) * i.+1 = \sum_(i < k) c i - k * c k.
proof: Proof. pose F i := c i * i.+1 - c i.+1 * i.+1. rewrite (eq_bigr (F \o val)) /=; first last. by move=> i _; rewrite mulnBl. rewrite [k * _]mulnC; elim: k=> [|k ih] h. by rewrite !big_ord0 muln0 subn0. rewrite !big_ord_recr /= ih; last first. by move=> i j /andP[le_ij lt_jSk]; rewrite h // le_ij leqW. rewrite {ih}/F addnBA ?leq_mul //; last by apply/h; rewrite leqnn ltnW. congr subn; rewrite addnC addnBA 1?addnC -?addnBA. + by rewrite -mulnBr subSnn muln1. + by rewrite leq_mul. elim: k h => [|k ih] h; first by rewrite muln0. rewrite big_ord_recr //= mulnS addnC leq_add //; last first. by apply/h; rewrite !ltnS !leqnSn. apply/leq_trans/ih; first by apply/leq_mul/leqnn/h; rewrite !ltnS leqnSn. by move=> i j /andP[le_ij lt_jSSk]; apply/h; rewrite le_ij !ltnS ltnW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)