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