proposition: Theorem schoice (A B : Type) (R : A -> B -> Prop) : (forall a : A, exists b : B , R a b) -> { f : A -> B | forall a : A, R a (f a) }.
proof: Proof. intros H. remember (func A B R H) as F. exists (ext_func A B R F). unfold ext_func. cbv; intuition. remember (F a) as W. destruct W. assumption. Qed.
imports: mathcomp(all_ssreflect all_algebra reals boolp)