proposition: Lemma descset_meet c1 c2 : descset (c1 `&` c2)%O = descset c1 :&: descset c2.
proof: Proof. by rewrite from_descsetK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype