proposition: Lemma sum_consecutive n f : fincr f -> f n = \sum_(0 <= i < n) (f i.+1 - f i) + f 0.
proof: Proof. move=> Hf. elim: n => [|n IH]; first by rewrite big_geq. by rewrite big_nat_recr //= addnAC -IH addnC subnK. Qed.
imports: mathcomp(all_ssreflect)