proposition: Lemma not_Empty_dec (E : R -> Prop) : (Decidable.decidable (exists x, E x)) -> {(exists x, E x)} + {(forall x, ~ E x)}.
proof: Proof. move => He ; case: (Empty_dec E) => Hx ; [left|right]. case: He => // He. contradict Hx ; apply: Empty_correct_2 => x ; contradict He ; by exists x. by apply: Empty_correct_1. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov