proposition: Lemma descsetK : cancel descset from_descset.
proof: Proof. case => [s Hs]; apply val_inj => /=. rewrite val_descset /=; move: Hs => /andP[/eqP Hsum Hcomp]. case: n Hsum => [/(comp0 Hcomp) -> // | n0]; set n' := n0.+1 => Hsum {Hcomp}. case: s Hsum => [|s0 s']//; move Hs: (s0 :: s') => s Hsum. have -> : rcons (partsums s) n' = [seq sumn (take i s) | i <- iota 1 (size s)]. rewrite /partsums -{}Hsum -Hs [size (s0 :: s')]/=. by rewrite -{2}(addn1 (size s')) iotaD /= map_cat /= take_size cats1. apply: (eq_from_nth (x0 := 0)) => [|i]; rewrite size_pairmap. by rewrite size_map size_iota. move=> Hi; rewrite (nth_pairmap 0) //; rewrite size_map size_iota in Hi. case: i Hi => [|i] /= Hi; first by rewrite -Hs /= take0 /= addn0 subn0. exact: diff_nth_sumn_take. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype