proposition: Lemma is_ub_Rbar_correct (E : R -> Prop) (l : Rbar) : is_ub_Rbar E l <-> Rbar_is_upper_bound (fun x => is_finite x /\ E x) l.
proof: Proof. split => [H x [<- Hx] | H x Hx] ; apply H => // ; by exists x. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov