proposition: Lemma Rbar_is_lub_subset (E1 E2 : Rbar -> Prop) (l1 l2 : Rbar) : (forall x, E1 x -> E2 x) -> (Rbar_is_lub E1 l1) -> (Rbar_is_lub E2 l2) -> Rbar_le l1 l2.
proof: Proof. intros Hs (_,H1) (H2, _). apply H1 ; intros x Hx ; apply H2, Hs, Hx. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov