proposition: Lemma select_pr (p : property) E: (exists2 x, inc x E & p x) -> (singl_val2 (inc ^~ E) p) -> (p (select p E) /\ inc (select p E) E).
proof: Proof. by move => [z ze pz] pc; rewrite -(select_uniq pc ze pz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)