proposition: Lemma singletonP x: singletonp x <-> (nonempty x /\ small_set x).
proof: Proof. split; first by move=> [z ->]; split;[fprops | apply: small1]. by move=> [[y yx] sx]; exists y; apply: (set1_pr yx) => z zx; apply: sx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)