proposition: Lemma Empty_dec (E : R -> Prop) : {~Empty E}+{Empty E}.
proof: Proof. case: (Rbar_eq_dec (Lub_Rbar (fun x => x = 0 \/ E x)) (Glb_Rbar (fun x => x = 0 \/ E x))) => H0 ; [ | left]. case: (Rbar_eq_dec (Lub_Rbar (fun x => x = 1 \/ E x)) (Glb_Rbar (fun x => x = 1 \/ E x))) => H1 ; [by right | left]. contradict H1 ; apply H1. contradict H0 ; apply H0. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov