proposition: Lemma mem_partsum_gt x v0 v1 v : v0 < x -> x \in partsums (v0 :: v1 :: v) -> x \in partsums (v0 + v1 :: v).
proof: Proof. move=> ltv0x. rewrite partsums_cons // inE (gtn_eqF ltv0x) /= => Hin. have Hv : v != [::] by move: Hin => /mapP[y /mem_partsum_non0]. move: Hin; rewrite !partsums_cons //= !inE -map_comp. move=> /orP[/eqP-> | /mapP[i Hin -> /=]]; first by rewrite eqxx. by rewrite addnA map_f ?orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype