proposition: Lemma uniq_enumP (T : eqType) e : uniq e -> e =i T -> axiom e.
proof: Proof. by move=> Ue sT x; rewrite count_uniq_mem ?sT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)