proposition: Lemma elt_enum_uniq : uniq elt_enum.
proof: Proof. have oK : ocancel (elt_g A B) (@elt_f K A B). by move=> [[x y]|] //=; case: eqP. by apply: pmap_uniq oK _ (enum_uniq _). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)