proposition: Lemma Rbar_ub_Finite (E : Rbar -> Prop) (l : R) : Rbar_is_upper_bound E l -> is_upper_bound (fun (x : R) => E x) l.
proof: Proof. intros H x Ex. now apply (H (Finite x)). Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov