proposition: Lemma Rbar_is_lb_subset (E1 E2 : Rbar -> Prop) (l : Rbar) : (forall x, E1 x -> E2 x) -> (Rbar_is_lower_bound E2 l) -> (Rbar_is_lower_bound E1 l).
proof: Proof. intros Hs Hl x Ex ; apply Hl, Hs ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov