proposition: Lemma card_descset c : #|descset c| = (size c).-1.
proof: Proof. have := congr1 size (val_descset c); rewrite size_map cardE => ->. by rewrite size_partsums. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype