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