proposition: Lemma descset_rowcompn : descset (rowcompn n) = set0.
proof: Proof. by apply/cards0_eq; rewrite card_descset /= /rowcomp; case n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype