proposition: Lemma all_exists_dichot2 (p: property) X: (forall x, inc x X -> ~ p x) \/ (exists2 x, inc x X & p x).
proof: Proof. case: (all_exists_dichot1 (fun z => ~ p z) X); [by left | move => h; right]. by case: h => x xE px; exists x => //; apply: excluded_middle. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)