proposition: Lemma Empty_correct_1 (E : R -> Prop) : Empty E -> forall x, ~ E x.
proof: Proof. case => E0 E1 x Ex. rewrite /Lub_Rbar /Glb_Rbar in E0 ; case : (ex_lub_Rbar (fun x : R => x = 0 \/ E x)) E0 => /= s0 Hs0 ; case : (ex_glb_Rbar (fun x : R => x = 0 \/ E x)) => i0 Hi0 /= E0. have : (x = 0) ; last move => {s0 Hs0 i0 Hi0 E0}. apply Rle_antisym. apply (Rbar_le_trans x s0 0). apply Hs0 ; by right. rewrite E0 ; apply Hi0 ; by left. apply (Rbar_le_trans 0 s0 x). apply Hs0 ; by left. rewrite E0 ; apply Hi0 ; by right. rewrite /Lub_Rbar /Glb_Rbar in E1 ; case : (ex_lub_Rbar (fun x : R => x = 1 \/ E x)) E1 => /= s1 Hs1 ; case : (ex_glb_Rbar (fun x : R => x = 1 \/ E x)) => i1 Hi1 /= E1. have : (x = 1) ; last move => {s1 Hs1 i1 Hi1 E1}. apply Rle_antisym. apply (Rbar_le_trans x s1 1). apply Hs1 ; by right. rewrite E1 ; apply Hi1 ; by left. apply (Rbar_le_trans 1 s1 x). apply Hs1 ; by left. rewrite E1 ; apply Hi1 ; by right. move => -> ; apply R1_neq_R0. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov