proposition: Lemma Rbar_glb_subset (E1 E2 : Rbar -> Prop) : (forall x, E2 x -> E1 x) -> Rbar_le (Rbar_glb E1) (Rbar_glb E2).
proof: Proof. intro Hs ; unfold Rbar_glb ; case (Rbar_ex_glb E1) ; intros l1 Hl1 ; case (Rbar_ex_glb E2) ; simpl ; intros l2 Hl2 ; apply (Rbar_is_glb_subset E1 E2) ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov