proposition: Lemma enum_uniq A : uniq (enum A).
proof: Proof. by apply/filter_uniq/count_mem_uniq => x; rewrite enumP -enumT mem_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)