proposition: Lemma subset1P X x : sub X (singleton x) <-> (X = emptyset \/ X = singleton x).
proof: Proof. split; last by case => ->; fprops. move => xsx; case: (emptyset_dichot X); first by left. by move => nea; right; apply: set1_pr1 => // z /xsx /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)