proposition: Lemma Empty_correct_2 (E : R -> Prop) : (forall x, ~ E x) -> Empty E.
proof: Proof. move => H ; split ; rewrite /Glb_Rbar /Lub_Rbar ; [ case : (ex_lub_Rbar (fun x : R => x = 0 \/ E x)) => s0 Hs0 ; case : (ex_glb_Rbar (fun x : R => x = 0 \/ E x)) => i0 Hi0 /= | case : (ex_lub_Rbar (fun x : R => x = 1 \/ E x)) => s1 Hs1 ; case : (ex_glb_Rbar (fun x : R => x = 1 \/ E x)) => i1 Hi1 /=]. have : (i0 = Finite 0) ; last move => -> ; apply: Rbar_le_antisym. apply Hi0 ; by left. apply Hi0 => y ; case => H0. rewrite H0 ; by right. contradict H0 ; apply H. apply Hs0 => y ; case => H0. rewrite H0 ; by right. contradict H0 ; apply H. apply Hs0 ; by left. have : (i1 = Finite 1) ; last move => -> ; apply: Rbar_le_antisym. apply Hi1 ; by left. apply Hi1 => y ; case => H1. rewrite H1 ; by right. contradict H1 ; apply H. apply Hs1 => y ; case => H1. rewrite H1 ; by right. contradict H1 ; apply H. apply Hs1 ; by left. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov