proposition: Lemma subseq_partsumE c1 c2 : (subseq (partsums c1) (partsums c2)) = (descset c1 \subset descset c2).
proof: Proof. apply/idP/subdescset_partsumP => [/mem_subseq // |]. by move/(sorted_subseqP ltn_trans ltnn); apply; apply: sorted_ltn_partsums. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype