proposition: Lemma fin_all_exists U (P : forall x : T, U x -> Prop) : (forall x, exists u, P x u) -> (exists u, forall x, P x (u x)).
proof: Proof. move=> ex_u; pose Q m x := enum_rank x < m -> {ux | P x ux}. suffices: forall m, m <= #|T| -> exists w : forall x, Q m x, True. case/(_ #|T|)=> // w _; pose u x := sval (w x (ltn_ord _)). by exists u => x; rewrite {}/u; case: (w x _). elim=> [|m IHm] ltmX; first by have w x: Q 0 x by []; exists w. have{IHm} [w _] := IHm (ltnW ltmX); pose i := Ordinal ltmX. have [u Pu] := ex_u (enum_val i); suffices w' x: Q m.+1 x by exists w'. rewrite /Q ltnS leq_eqVlt (val_eqE _ i); case: eqP => [def_i _ | _ /w //]. by rewrite -def_i enum_rankK in u Pu; exists u. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)