proposition: Lemma sum_diff_tuple t : sorted leq t -> forall i, i < d.+1 -> \sum_(0 <= j < i) (nth 0 t j.+1 - nth 0 t j) = nth 0 t i - nth 0 t 0.
proof: Proof. move=> /(sorted2P 0 leq_trans leqnn) srt. elim=> [|i IHi] ltid; first by rewrite big_nil subnn. rewrite big_nat_recr //= IHi; last exact: ltnW. rewrite addnC addnBA ?srt ?size_tuple //=; last exact: ltnW. by rewrite subnK // srt // size_tuple leqnSn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype