proposition: Lemma is_ub_Rbar_subset (E1 E2 : R -> Prop) (l : Rbar) : (forall x : R, E2 x -> E1 x) -> is_ub_Rbar E1 l -> is_ub_Rbar E2 l.
proof: Proof. move => H ub1 x Hx. apply: ub1 ; by apply: H. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov