proposition: Lemma up_choice: choiceA U inc'.
proof: Proof. move:up_values => [Ev _ _ _ [_ dv]]. rewrite /choiceA => x _ pa pb. set E := fun_image (f x) f. have p1: (forall z, inc z E -> nonempty z). move => z /funI_P [y /(pa _ (up_Ut y)) h ->]. by case: (emptyset_dichot (f y)) => // fe; case h;rewrite Ev - (gf y) fe. have p2:(forall z z', inc z E -> inc z' E -> z = z' \/ disjoint z z'). move => z z' /funI_P [y fyx ->] /funI_P [y' fyx' ->]. move:(pb _ _ (up_Ut y) (up_Ut y') fyx fyx'). rewrite up_disjoint;case; [ by move => ->; left | by right]. move: AC_variants => [_ [_ ac3]]. have: (forall x, exists r, forall z, inc z x -> nonempty z -> inc (r z) z). by move => X; exists rep => y _ ney; apply:rep_i. move /ac3 => AC; move: (AC E p1 p2) => [y yp]; clear AC ac3. exists (g y) => //. move => z _ zx. have fze: inc (f z) E by apply /funI_P; exists z. by move: (yp _ fze) => [t]; move => h; exists t => //;rewrite up_inter2 fg dv h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)