proposition: Lemma count_enumP : axiom count_enum.
proof: Proof. apply: uniq_enumP (pmap_uniq (@pickle_invK T) (iota_uniq _ _)) _ => x. by rewrite mem_pmap -pickleK_inv map_f // mem_iota ubT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)