proposition: Lemma small_set_pr x: small_set x -> x = emptyset \/ singletonp x.
proof: Proof. move=> sx; case: (emptyset_dichot x); first by left. by move=> ne; right; apply/singletonP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)