proposition: Lemma sorted_ltn_partsums c : sorted ltn (partsums c).
proof: Proof. case: c => [c /= /andP[_ /is_compP Hcomp]]. apply/(sortedP 0) => i. rewrite size_map size_iota /= -[nth _ _ _ < _]subn_gt0 => Hi. rewrite diff_nth_sumn_take ?leq_pred // lt0n. apply: Hcomp; apply: mem_nth. by case: (size c) Hi => //= sz /ltn_trans; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype