proposition: Lemma all_exists_dichot1 (p: property) X: (forall x, inc x X -> p x) \/ (exists2 x, inc x X & ~p x).
proof: Proof. case: (emptyset_dichot (Zo X (fun z => ~ p z))). move => ze;left => x xX; ex_middle bad; case:(@in_set0 x). by rewrite - ze; apply: Zo_i. by move => [x /Zo_P[ga gb]]; right; exists x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)