proposition: Lemma mem_partsum_non0 u0 u i : i \in partsums (u0 :: u) -> u != [::].
proof: Proof. by move => Hi; apply/negP => /eqP Hu; rewrite Hu /partsums /= in Hi. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype