proposition: Lemma existsTP (P : T -> Prop) : { x : T | P x } + (forall x, ~ P x).
proof: Proof. case: (boolP `[<exists x : T, P x>]) => [/exists_asboolP | /asboolPn] h. by case/cid: h => w Pw; left; exists w; apply/asboolP. by right=> x Px; apply/h; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap reals