proposition: Lemma partsums_cons i s : s != [::] -> partsums (i :: s) = i :: [seq i + j | j <- partsums s].
proof: Proof. move=> /(partsums_cat (s1 := [:: i]) is_true_true) /= ->. by rewrite addn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype