proposition: Lemma topEcompnref : 1%O = colcompn n :> 'CRef.
proof: Proof. by apply: descset_inj; rewrite from_descsetK descset_colcompn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype