proposition: Lemma classical_denumerable_description_imp_fun_choice : forall A:Type, FunctionalRelReification_on A nat -> forall R:A->nat->Prop, (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R.
proof: Proof. intros A Descr. red; intros R Rdec H. set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y'). destruct (Descr R') as (f,Hf). - intro x. apply (dec_inh_nat_subset_has_unique_least_element (R x)). + apply Rdec. + apply (H x). - exists f. intros x. destruct (Hf x) as (Hfx,_). assumption. Qed.
imports: RelationClasses Logic Wf_nat Decidable