proposition: Lemma all_partsums c : all (fun i => 0 < i < n) (partsums c).
proof: Proof. rewrite all_map; apply/allP => i; rewrite mem_iota add1n. case: c => [[|c0 c]] /andP[/eqP <-]/=; first by case: i. rewrite is_comp_cons -lt0n => /andP[Hc0 Hc]. case: i => //= i /ltnSE ltisz. rewrite (leq_trans Hc0) ?leq_addr //= ltn_add2l {c0 Hc0}. rewrite -{2}(cat_take_drop i c) sumn_cat -addn1 leq_add2l. rewrite (drop_nth 0 ltisz) /= (leq_trans _ (leq_addr _ _)) // lt0n. by move: Hc; apply contra => /eqP <-; exact: mem_nth. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype