proposition: Lemma descset_colcompn : descset (colcompn n) = setT.
proof: Proof. apply/eqP; rewrite -subset_leqif_cards; last exact: subsetT. by rewrite card_descset /= /colcomp /= size_nseq cardsT card_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype