proposition: Lemma val_descset c : [seq (val i).+1 | i in descset c] = partsums c.
proof: Proof. apply: (irr_sorted_eq (ltn_trans) ltnn). - rewrite sorted_map (eq_sorted (e' := fun i j => val i < val j)). rewrite /enum_mem -enumT /= sorted_filter // ?enum_ord_sorted_ltn //. by move=> i j k /ltn_trans; apply. - by move=> i j /=; rewrite ltnS. - exact: sorted_ltn_partsums. move=> i; apply/mapP/idP => [[/= [x Hx]] | Hi]. - rewrite mem_enum /descset inE mem_pmap_sub /=. move/mapP => [/= j Hj ->{x Hx} ->{i}]. by have /= /allP/(_ _ Hj) := all_partsums c; case: j Hj. - have /= /allP/(_ _ Hi) lt0in := all_partsums c. have ltin : i.-1 < n.-1 by case: n i lt0in {Hi} => [|n0][|i]. exists (Ordinal ltin) => /=; last by case: i lt0in {Hi ltin}. rewrite mem_enum /descset inE /= mem_pmap_sub /=. by apply/mapP; exists i. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype