proposition: Lemma ex_middle_pick (P: T1 -> Prop): ex_middle -> (exists x, (T1nf x /\ P x)) \/ (forall x, T1nf x -> ~ (P x)).
proof: Proof. move => h. by case (h P); [left |move => nq; right => x nx px; case nq; exists x ]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)