proposition: Lemma from_descsetK : cancel from_descset descset.
proof: Proof. by rewrite (bij_can_sym descset_bij); exact: descsetK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype