proposition: Lemma descset_bij : bijective descset.
proof: Proof. apply: (inj_card_bij descset_inj); rewrite /= card_intcompn. by rewrite -cardsT -powersetT card_powerset cardsT card_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype