proposition: Lemma select_uniq (p: property) E: (singl_val2 (inc ^~ E) p) -> forall x, inc x E -> p x -> x = (select p E).
proof: Proof. move => h x xE px; rewrite /select. suff: (Zo E p) = singleton x by move => ->; rewrite setU_1. by apply: set1_pr; [ apply: Zo_i | move => z; case/Zo_P => ze pz; apply: h]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)