proposition: Lemma is_lub_Rbar_subset (E1 E2 : R -> Prop) (l1 l2 : Rbar) : (forall x : R, E2 x -> E1 x) -> is_lub_Rbar E1 l1 -> is_lub_Rbar E2 l2 -> Rbar_le l2 l1.
proof: Proof. move => H [ub1 _] [_ lub2]. apply: lub2 ; by apply (is_ub_Rbar_subset E1), ub1. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov