src/HOL/Library/Countable_Set.thy

   ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \<circ> f) S UNIV"
     by (rule bij_betw_trans)
   then show thesis ..
 qed
 
+lemma countable_infiniteE':
+  assumes "countable A" "infinite A"
+  obtains g where "bij_betw g (UNIV :: nat set) A"
+  using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast
+
 lemma countable_enum_cases:
   assumes "countable S"
   obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"
         | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV"
   using ex_bij_betw_finite_nat[of S] countableE_infinite \<open>countable S\<close>