proposition: Lemma choice_imply_dep_choice : exists f, IS R f.
proof: Proof. destruct (choice G G_is_classic_left_total) as [f H]. exists f. assert (forall i x, G i x -> x = f i). intros. ded (H i). exact (G_is_functional H0 H1). assert (f 0 = a). ded (H 0). inversion H1. refl. assert (forall i, f (S i) = next_elt (f i)). induction i. ded (H 1). inversion H2. inversion H5. rewrite H1. subst x. refl. ded (H (S (S i))). inversion H2. ded (H0 _ _ H5). subst x. refl. intro. rewrite H2. exact (proj2_sig (h (f i))). Qed.
imports: Coq(ClassicalChoice) CoLoR(RelUtil LogicUtil)