proposition: Fact xchoose_subproof P exP : {x | find P (ex_minn (@choice_complete_subdef _ P exP)) = Some x}.
proof: Proof. case: (ex_minnP (complete exP)) => n. by case: (find P n) => // x; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)