proposition: Lemma emptyset_dichot x: x = emptyset \/ nonempty x.
proof: Proof. case: (p_or_not_p (nonempty x)); [ by right | move => nex; left]. by apply /set0_P => t tx; case: nex; exists t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)