proposition: Lemma fin_choice (X : finType) Y (R : X -> Y -> Prop) : (forall x : X , exists y , R x y) -> exists f, forall x , R x (f x).
proof: Proof. case n : (#|X|) => [|m]. - have F : X -> False. move => x. move : (max_card (pred1 x)). by rewrite card1 n. exists (fun x => match F x with end) => x. done. - move => step. have H : forall x, x \in enum X -> exists y, R x y. by move => *. case (step (cardSmC n)) => d. move/(fin_choice_aux d) : H => [f Hf]. exists f => x. apply: Hf. by rewrite mem_enum. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)