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