"countable choice" according to wikipedia

countable_choice_wikipedia.v

(* P is a family of nat-indexed sets of nat such that:
   H: for all n, there is an m such that m ∈ P n
   -----------
   Then we show that there is a choice function f
*)
Theorem countable_choice_wikipedia
  (P : nat -> (nat -> Prop)) (H : forall n, { m | P n m }) : { f | forall n, (exists m, P n m /\ f n = m)}.
Proof.
  set (f := fun (n : nat) => let (m, Hm) := H n in m).
  exists f.
  intros n. exists (f n).
  split; auto.
  unfold f. now destruct (H n) as [m' Hm'].
Qed.