proposition: Lemma diff_nth_sumn_take s i m : m <= size s -> i.+1 < m -> nth 0 [seq sumn (take i0 s) | i0 <- iota 1 m] i.+1 - nth 0 [seq sumn (take i0 s) | i0 <- iota 1 m] i = nth 0 s i.+1.
proof: Proof. move=> Hm Hi. rewrite !(nth_map 0) ?size_iota //=; last exact: (ltn_trans _ Hi). rewrite !nth_iota //=; last exact: (ltn_trans _ Hi). rewrite !add1n !sumn_take [X in X - _]big_nat_recr //=. by rewrite addnC addnK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype