proposition: Lemma pcan_enumP g : pcancel f g -> Finite.axiom (undup (pmap g (enumF fT))).
proof: Proof. move=> fK x; rewrite count_uniq_mem ?undup_uniq // mem_undup. by rewrite mem_pmap -fK map_f // -enumT mem_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)