(**
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/

Copyright (C) 2011-2015 Sylvie Boldo
#<br />#
Copyright (C) 2011-2015 Catherine Lelay
#<br />#
Copyright (C) 2011-2015 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

Require Import Reals mathcomp.ssreflect.ssreflect.
Require Import Rbar Rcomplements Markov.

(** This file gives properties of (least) upper and (greatest) lower
bounds, especially in [Rbar].
- There are links between our bounds on [Rbar] and those of the
standard library on [R]: for example Lemma [Rbar_ub_R_ub] between our
[Rbar_is_upper_bound] and the standard library [is_upper_bound].
- From [Markov]'s principle, we deduce the construction of a lub (and
of a glb) in [Rbar] from any non-empty set of reals: see Lemma
[ex_lub_Rbar_ne].  *)

Open Scope R_scope.

(** * Bounds for sets in [R] *)
(** ** Upper and Lower bounds *)

Definition is_ub_Rbar (E : R -> Prop) (l : Rbar) :=
  forall (x : R), E x -> Rbar_le x l.
Definition is_lb_Rbar (E : R -> Prop) (l : Rbar) :=
  forall (x : R), E x -> Rbar_le l x.

Lemma is_ub_Rbar_opp (E : R -> Prop) (l : Rbar) :
  is_lb_Rbar E l <-> is_ub_Rbar (fun x => E (- x)) (Rbar_opp l).
Proof.
(* Goal: iff (is_ub_Rbar E l) (is_lb_Rbar (fun x : R => E (Ropp x)) (Rbar_opp l)) *)
  split ; intros Hl x Hx ; apply Rbar_opp_le.
(* Goal: Rbar_le (Rbar_opp (Finite x)) (Rbar_opp (Rbar_opp l)) *)
(* Goal: Rbar_le (Rbar_opp l) (Rbar_opp (Finite x)) *)
  now rewrite Rbar_opp_involutive ; apply Hl.
(* Goal: Rbar_le (Rbar_opp l) (Rbar_opp (Finite x)) *)
  now apply Hl ; rewrite Ropp_involutive.
Qed.
Lemma is_lb_Rbar_opp (E : R -> Prop) (l : Rbar) :
  is_ub_Rbar E l <-> is_lb_Rbar (fun x => E (- x)) (Rbar_opp l).
Proof.
(* Goal: iff (is_ub_Rbar E l) (is_lb_Rbar (fun x : R => E (Ropp x)) (Rbar_opp l)) *)
  split ; intros Hl x Hx ; apply Rbar_opp_le.
(* Goal: Rbar_le (Rbar_opp (Finite x)) (Rbar_opp (Rbar_opp l)) *)
(* Goal: Rbar_le (Rbar_opp l) (Rbar_opp (Finite x)) *)
  now rewrite Rbar_opp_involutive ; apply Hl.
(* Goal: Rbar_le (Rbar_opp l) (Rbar_opp (Finite x)) *)
  now apply Hl ; rewrite Ropp_involutive.
Qed.

(** Decidability *)

Lemma is_ub_Rbar_dec (E : R -> Prop) :
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  {l : R | is_ub_Rbar E l} + {(forall l : R, ~is_ub_Rbar E l)}.
Proof.
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
  set (F (n : nat) (x : R) := x = 0 \/ (E x /\ x <= INR n)).
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
  assert (F_b : forall n, bound (F n)).
(* Goal: forall n : nat, bound (F n) *)
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
    intros ; exists (INR n) => x ; case => [-> | Hx].
(* Goal: Rbar_le (Finite x) b *)
    by apply pos_INR.
(* Goal: Rbar_le (Finite x) b *)
    by apply Hx.
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
  assert (F_ex : forall n, (exists x : R, F n x)).
(* Goal: forall n : nat, @ex R (fun x : R => F n x) *)
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
    intros ; exists 0 ; by left.
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
  set (u (n : nat) := proj1_sig (completeness (F n) (F_b n) (F_ex n))).
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
  destruct (LPO_ub_dec u) as [ [M HM] | HM].
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  + left ; exists M => x Hx.
(* Goal: Rbar_le (Finite x) (Finite M) *)
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
    destruct (nfloor_ex (Rmax 0 x)) as [n Hn].
(* Goal: Rbar_le (Finite x) b *)
    by apply Rmax_l.
(* Goal: Rbar_le (Finite x) (Finite M) *)
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
    eapply Rle_trans, (HM (S n)).
(* Goal: Rgt (u (S n)) (Ropp (INR (S n))) *)
    rewrite /u ; case: completeness => l Hl /=.
(* Goal: Rle x l *)
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
    apply Hl ; right ; split => //.
(* Goal: Rle x (INR (S n)) *)
(* Goal: sumor (@sig R (fun l : R => is_ub_Rbar E (Finite l))) (forall l : R, not (is_ub_Rbar E (Finite l))) *)
    rewrite S_INR ; eapply Rle_trans, Rlt_le, Hn.
(* Goal: Rbar_le (Finite x) b *)
    by apply Rmax_r.
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  + right => l Hl.
(* Goal: P (real (Lub_Rbar P)) *)
    case: (HM (Rmax 0 l)) => n {HM}.
(* Goal: not (Rlt (Ropp (INR n)) l) *)
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    apply Rle_not_lt.
(* Goal: Rgt (u (S n)) (Ropp (INR (S n))) *)
    rewrite /u ; case: completeness => M HM /=.
(* Goal: bound (E m) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    apply HM => x ; case => [ -> | Hx].
(* Goal: Rbar_le (Finite x) b *)
    by apply Rmax_l.
(* Goal: Rle x (Rmax (IZR Z0) l) *)
    eapply Rle_trans, Rmax_r.
(* Goal: Rle x l *)
    apply Hl, Hx.
Qed.

Lemma is_lb_Rbar_dec (E : R -> Prop) :
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  {l : R | is_lb_Rbar E l} + {(forall l : R, ~is_lb_Rbar E l)}.
Proof.
(* Goal: sumor (@sig R (fun l : R => is_lb_Rbar E (Finite l))) (forall l : R, not (is_lb_Rbar E (Finite l))) *)
  destruct (is_ub_Rbar_dec (fun x => E (- x))) as [ [l Hl] | Hl ].
(* Goal: sumor (@sig R (fun l : R => is_lb_Rbar E (Finite l))) (forall l : R, not (is_lb_Rbar E (Finite l))) *)
(* Goal: sumor (@sig R (fun l : R => is_lb_Rbar E (Finite l))) (forall l : R, not (is_lb_Rbar E (Finite l))) *)
  left ; exists (Rbar_opp l).
(* Goal: Rbar_le (Finite x) b *)
  by apply is_ub_Rbar_opp ; rewrite (Rbar_opp_involutive l).
(* Goal: Rbar_le l b *)
  right => l.
(* Goal: not (is_lb_Rbar E (Finite l)) *)
  specialize (Hl (Rbar_opp l)).
(* Goal: not (is_lb_Rbar E (Finite l)) *)
  contradict Hl.
(* Goal: Rbar_le (Finite x) b *)
  by apply (is_ub_Rbar_opp E l).
Qed.

(** Order *)

Lemma is_ub_Rbar_subset (E1 E2 : R -> Prop) (l : Rbar) :
  (forall x : R, E2 x -> E1 x) -> is_ub_Rbar E1 l -> is_ub_Rbar E2 l.
Proof.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => H ub1 x Hx.
(* Goal: Rbar_le l1 l2 *)
  apply: ub1 ; by apply: H.
Qed.
Lemma is_lb_Rbar_subset (E1 E2 : R -> Prop) (l : Rbar) :
  (forall x : R, E2 x -> E1 x) -> is_lb_Rbar E1 l -> is_lb_Rbar E2 l.
Proof.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => H ub1 x Hx.
(* Goal: Rbar_le l1 l2 *)
  apply: ub1 ; by apply: H.
Qed.

(** ** Least upper bound and Greatest Lower Bound *)

Definition is_lub_Rbar (E : R -> Prop) (l : Rbar) :=
  is_ub_Rbar E l /\ (forall b, is_ub_Rbar E b -> Rbar_le l b).
Definition is_glb_Rbar (E : R -> Prop) (l : Rbar) :=
  is_lb_Rbar E l /\ (forall b, is_lb_Rbar E b -> Rbar_le b l).

Lemma is_lub_Rbar_opp (E : R -> Prop) (l : Rbar) :
  is_glb_Rbar E l <-> is_lub_Rbar (fun x => E (- x)) (Rbar_opp l).
Proof.
(* Goal: iff (is_lub_Rbar E l) (is_glb_Rbar (fun x : R => E (Ropp x)) (Rbar_opp l)) *)
  split => [[lb glb] | [ub lub] ] ; split.
(* Goal: Rbar_le (Finite x) b *)
  by apply is_ub_Rbar_opp.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
  intros b Hb.
(* Goal: Rbar_le b (Rbar_opp l) *)
(* Goal: is_ub_Rbar E l *)
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar E b), Rbar_le l b *)
  apply Rbar_opp_le ; rewrite Rbar_opp_involutive.
(* Goal: Rbar_le (Rbar_opp b) l *)
(* Goal: is_lb_Rbar E l *)
(* Goal: forall (b : Rbar) (_ : is_lb_Rbar E b), Rbar_le b l *)
  apply glb, is_ub_Rbar_opp ; by rewrite Rbar_opp_involutive.
(* Goal: Rbar_le (Finite x) b *)
  by apply is_ub_Rbar_opp.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
  intros b Hb.
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Rbar_opp_le.
(* Goal: Rbar_le (Finite x) b *)
  by apply lub, is_ub_Rbar_opp.
Qed.
Lemma is_glb_Rbar_opp (E : R -> Prop) (l : Rbar) :
  is_lub_Rbar E l <-> is_glb_Rbar (fun x => E (- x)) (Rbar_opp l).
Proof.
(* Goal: iff (is_lub_Rbar E l) (is_glb_Rbar (fun x : R => E (Ropp x)) (Rbar_opp l)) *)
  split => [[lb glb] | [ub lub] ] ; split.
(* Goal: Rbar_le (Finite x) b *)
  by apply is_lb_Rbar_opp.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
  intros b Hb.
(* Goal: Rbar_le b (Rbar_opp l) *)
(* Goal: is_ub_Rbar E l *)
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar E b), Rbar_le l b *)
  apply Rbar_opp_le ; rewrite Rbar_opp_involutive.
(* Goal: Rbar_le l (Rbar_opp b) *)
(* Goal: is_ub_Rbar E l *)
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar E b), Rbar_le l b *)
  apply glb, is_lb_Rbar_opp ; by rewrite Rbar_opp_involutive.
(* Goal: Rbar_le (Finite x) b *)
  by apply is_lb_Rbar_opp.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
  intros b Hb.
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Rbar_opp_le.
(* Goal: Rbar_le (Finite x) b *)
  by apply lub, is_lb_Rbar_opp.
Qed.

(** Existence *)

Lemma ex_lub_Rbar (E : R -> Prop) : {l : Rbar | is_lub_Rbar E l}.
Proof.
  destruct (is_ub_Rbar_dec E)  as [[M HM] | HM] ; first last.
(* sup = p_infty *)
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_lub E l) *)
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_lub E l) *)
  exists p_infty ; split.
(* Goal: Rbar_le (Finite x) b *)
  by [].
  case => [l | | ] // Hl.
(* Goal: Rbar_le (Finite x) b *)
  by specialize (HM l).
(* Goal: Rbar_le p_infty m_infty *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar E l) *)
  specialize (HM 0).
(* Goal: Rbar_le l b *)
  contradict HM => x Hx.
(* Goal: Rbar_le (Finite x) b *)
  by specialize (Hl x Hx).

(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar E l) *)
rename E into F.
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  assert (F_b : bound F).
(* Goal: Rbar_le l b *)
    exists M => x Hx.
(* Goal: Rbar_le (Finite x) b *)
    by apply HM.
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    clear -F_b.

(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  set (E (m : nat) (x : R) := x = - INR m \/ F x).
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  assert (E_b : forall m, bound (E m)).
(* Goal: forall m : nat, bound (E m) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    intros m.
(* Goal: P (real (Lub_Rbar P)) *)
    case: F_b => l Hl.
(* Goal: bound (E m) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    exists (Rmax l (- INR m)) => x ; case => [ -> | Hx].
(* Goal: Rbar_le (Finite x) b *)
    by apply Rmax_r.
(* Goal: Rle x (Rmax l (Ropp (INR m))) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    eapply Rle_trans, Rmax_l.
(* Goal: Rbar_le (Finite x) b *)
    by apply Hl.
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  assert (E_ex : forall m, exists x : R, E m x).
(* Goal: forall m : nat, @ex R (fun x : R => E m x) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    intros m ; exists (- INR m) ; by left.
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  set (u m := proj1_sig (completeness (E m) (E_b m) (E_ex m))).

(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  destruct (LPO (fun n => u n <> - INR n)) as [ [n Hn] | Hn].
(* Goal: forall n : nat, @eq R (u n) (Ropp (INR n)) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    intros n.
(* Goal: P (real (Lub_Rbar P)) *)
    case: (Req_EM_T (u n) (- INR n)) => H.
(* Goal: Rbar_le (Finite x) b *)
    by right.
(* Goal: Rbar_le (Finite x) b *)
    by left.
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  exists (u n).
(* Goal: forall _ : forall x : R, iff (E1 x) (E2 x), @eq Rbar (Glb_Rbar E1) (Glb_Rbar E2) *)
  move: Hn ; rewrite /u ; case: completeness => l Hl /= H.
(* Goal: is_lub_Rbar P (Finite x) *)
  split.
(* Goal: is_upper_bound (E n) (Ropp (INR n)) *)
(* Goal: E n (Ropp (INR n)) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  intros x Hx.
(* Goal: Rbar_le (Finite x) b *)
  apply Hl ; by right.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar F b), Rbar_le (Finite l) b *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  assert (- INR n < l).
(* Goal: P (real (Lub_Rbar P)) *)
  case: Hl => Hl _.
(* Goal: P (real (Lub_Rbar P)) *)
  case: (Hl (-INR n)) => //=.
(* Goal: Rbar_le (Finite x) b *)
  by left.
(* Goal: forall _ : @eq R (Ropp (INR n)) l, Rlt (Ropp (INR n)) l *)
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar F b), Rbar_le (Finite l) b *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  intros H0 ; contradict H.
(* Goal: Rbar_le (Finite x) b *)
  by rewrite -H0.
(* Goal: P (real (Lub_Rbar P)) *)
  case => [b | | ] //= Hb.
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  + apply Hl => x Hx.
(* Goal: forall _ : @eq R x (IZR Z0), False *)
    case: Hx => Hx ; first last.
(* Goal: Rbar_le (Finite x) b *)
    by apply Hb.
(* Goal: @eq Rbar (Rbar_glb E) l *)
    rewrite Hx.
(* Goal: Rle (Ropp (INR n)) b *)
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    apply Rnot_lt_le ; contradict H0.
(* Goal: not (Rlt (Ropp (INR n)) l) *)
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    apply Rle_not_lt.
(* Goal: Rbar_le l b *)
    apply Hl => y Hy.
(* Goal: P (real (Lub_Rbar P)) *)
    case: Hy => Hy.
(* Goal: Rle y (Ropp (INR n)) *)
(* Goal: Rle y (Ropp (INR n)) *)
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    rewrite Hy ; apply Rle_refl.
(* Goal: Rle y (Ropp (INR n)) *)
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    eapply Rle_trans, Rlt_le, H0.
(* Goal: Rbar_le (Finite x) b *)
    by apply Hb.
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  + contradict H.
(* Goal: @eq R l (Ropp (INR n)) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    apply Rle_antisym ; apply Hl.
(* Goal: is_upper_bound (E n) (Ropp (INR n)) *)
(* Goal: E n (Ropp (INR n)) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    intros x Hx.
(* Goal: P (real (Lub_Rbar P)) *)
    case: Hx => [-> | Hx] //.
(* Goal: Rbar_le (Finite x) b *)
    by apply Rle_refl.
(* Goal: Rbar_le (Finite x) b *)
    by apply Hb in Hx.
(* Goal: Rbar_le (Finite x) b *)
    by left.
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  assert (forall n, u n = - INR n).
(* Goal: forall n : nat, @eq R (u n) (Ropp (INR n)) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    intros n.
(* Goal: @eq R (u n) (Ropp (INR n)) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    specialize (Hn n).
(* Goal: P (real (Lub_Rbar P)) *)
    case: (Req_dec (u n) (- INR n)) => // H.
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    clear Hn.
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  exists m_infty ; split => // x Hx.
(* Goal: Rbar_le (Finite x) m_infty *)
  destruct (nfloor_ex (Rmax 0 (- x))) as [n Hn].
(* Goal: Rbar_le (Finite x) b *)
  by apply Rmax_l.
(* Goal: Rbar_le (Finite x) m_infty *)
  specialize (H (S n)).
(* Goal: Rbar_le (Finite x) m_infty *)
  contradict H.
(* Goal: not (@eq R (u (S n)) (Ropp (INR (S n)))) *)
  apply Rgt_not_eq.
(* Goal: Rgt (u (S n)) (Ropp (INR (S n))) *)
  rewrite /u S_INR ; case: completeness => l Hl /=.
(* Goal: Rgt l (Ropp (Rplus (INR n) (IZR (Zpos xH)))) *)
  eapply Rlt_le_trans with x.
(* Goal: Rlt (Ropp (Rplus (INR n) (IZR (Zpos xH)))) x *)
(* Goal: Rle x l *)
  apply Ropp_lt_cancel ; rewrite Ropp_involutive.
(* Goal: Rlt (Ropp x) (Rplus (INR n) (IZR (Zpos xH))) *)
(* Goal: Rle x l *)
  eapply Rle_lt_trans, Hn.
(* Goal: Rbar_le (Finite x) b *)
  by apply Rmax_r.
(* Goal: Rbar_le (Rbar_opp l) (Rbar_opp x) *)
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Hl.
(* Goal: Rbar_le (Finite x) b *)
  by right.
Qed.
Lemma ex_glb_Rbar (E : R -> Prop) : {l : Rbar | is_glb_Rbar E l}.
Proof.
(* Goal: P (real (Lub_Rbar P)) *)
  case: (ex_lub_Rbar (fun x => E (- x))) => l Hl.
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_glb E l) *)
  exists (Rbar_opp l).
(* Goal: is_glb_Rbar E (Rbar_opp l) *)
  apply is_lub_Rbar_opp ; by rewrite Rbar_opp_involutive.
Qed.

(** Functions *)

Definition Lub_Rbar (E : R -> Prop) := proj1_sig (ex_lub_Rbar E).
Definition Glb_Rbar (E : R -> Prop) := proj1_sig (ex_glb_Rbar E).

Lemma is_lub_Rbar_unique (E : R -> Prop) (l : Rbar) :
  is_lub_Rbar E l -> Lub_Rbar E = l.
Proof.
(* Goal: forall _ : forall x : R, iff (E1 x) (E2 x), @eq Rbar (Glb_Rbar E1) (Glb_Rbar E2) *)
  move => Hl ; rewrite /Lub_Rbar ; case: ex_lub_Rbar => l' /= Hl'.
(* Goal: @eq Rbar l0 l *)
  apply Rbar_le_antisym.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hl', Hl.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hl, Hl'.
Qed.
Lemma is_glb_Rbar_unique (E : R -> Prop) (l : Rbar) :
  is_glb_Rbar E l -> Glb_Rbar E = l.
Proof.
(* Goal: forall _ : forall x : R, iff (E1 x) (E2 x), @eq Rbar (Glb_Rbar E1) (Glb_Rbar E2) *)
  move => Hl ; rewrite /Glb_Rbar ; case: ex_glb_Rbar => l' /= Hl'.
(* Goal: @eq Rbar l0 l *)
  apply Rbar_le_antisym.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hl, Hl'.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hl', Hl.
Qed.

Lemma Lub_Rbar_correct (E : R -> Prop) :
  is_lub_Rbar E (Lub_Rbar E).
Proof.
(* Goal: is_glb_Rbar E (Glb_Rbar E) *)
  rewrite /Lub_Rbar ; by case: ex_lub_Rbar => l /= Hl.
Qed.
Lemma Glb_Rbar_correct (E : R -> Prop) :
  is_glb_Rbar E (Glb_Rbar E).
Proof.
(* Goal: is_glb_Rbar E (Glb_Rbar E) *)
  rewrite /Glb_Rbar ; by case: ex_glb_Rbar => l /= Hl.
Qed.

(** Order *)

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.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => H [ub1 _] [_ lub2].
(* Goal: Rbar_le l1 l2 *)
  apply: lub2 ; by apply (is_ub_Rbar_subset E1), ub1.
Qed.
Lemma is_glb_Rbar_subset (E1 E2 : R -> Prop) (l1 l2 : Rbar) :
  (forall x : R, E2 x -> E1 x) -> is_glb_Rbar E1 l1 -> is_glb_Rbar E2 l2
    -> Rbar_le l1 l2.
Proof.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => H [ub1 _] [_ lub2].
(* Goal: Rbar_le l1 l2 *)
  apply: lub2 ; by apply (is_lb_Rbar_subset E1), ub1.
Qed.

Lemma is_lub_Rbar_eqset (E1 E2 : R -> Prop) (l : Rbar) :
  (forall x : R, E2 x <-> E1 x) -> is_lub_Rbar E1 l -> is_lub_Rbar E2 l.
Proof.
(* Goal: is_lub_Rbar P (Finite x) *)
  move => H [ub1 lub1] ; split.
(* Goal: is_ub_Rbar E2 l *)
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar E2 b), Rbar_le l b *)
  apply (is_ub_Rbar_subset E1) ; [apply H | apply ub1].
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar E2 b), Rbar_le l b *)
  move => b Hb ; apply: lub1 ; apply (is_ub_Rbar_subset E2) ; [apply H | apply Hb].
Qed.
Lemma is_glb_Rbar_eqset (E1 E2 : R -> Prop) (l : Rbar) :
  (forall x : R, E2 x <-> E1 x) -> is_glb_Rbar E1 l -> is_glb_Rbar E2 l.
Proof.
(* Goal: is_lub_Rbar P (Finite x) *)
  move => H [ub1 lub1] ; split.
(* Goal: is_lb_Rbar E2 l *)
(* Goal: forall (b : Rbar) (_ : is_lb_Rbar E2 b), Rbar_le b l *)
  apply (is_lb_Rbar_subset E1) ; [apply H | apply ub1].
(* Goal: forall (b : Rbar) (_ : is_lb_Rbar E2 b), Rbar_le b l *)
  move => b Hb ; apply: lub1 ; apply (is_lb_Rbar_subset E2) ; [apply H | apply Hb].
Qed.

Lemma Lub_Rbar_eqset (E1 E2 : R -> Prop) :
  (forall x, E1 x <-> E2 x) -> Lub_Rbar E1 = Lub_Rbar E2.
Proof.
  move => H ; rewrite {2}/Lub_Rbar ;
  case: ex_lub_Rbar => l /= Hl.
(* Goal: @eq Rbar (Lub_Rbar E1) l *)
  apply is_lub_Rbar_unique.
(* Goal: is_glb_Rbar E1 l2 *)
  move: Hl ; by apply is_lub_Rbar_eqset.
Qed.
Lemma Glb_Rbar_eqset (E1 E2 : R -> Prop) :
  (forall x, E1 x <-> E2 x) -> Glb_Rbar E1 = Glb_Rbar E2.
Proof.
  move => H ; rewrite {2}/Glb_Rbar ;
  case: (ex_glb_Rbar E2) => l2 H2 /=.
(* Goal: @eq Rbar (Glb_Rbar E1) l2 *)
  apply is_glb_Rbar_unique.
(* Goal: is_glb_Rbar E1 l2 *)
  move: H2 ; by apply is_glb_Rbar_eqset.
Qed.

(** * Bounds for sets in [Rbar] *)
(** ** Upper and Lower bounds *)

Definition Rbar_is_upper_bound (E : Rbar -> Prop) (l : Rbar) :=
  forall x, E x -> Rbar_le x l.

Definition Rbar_is_lower_bound (E : Rbar -> Prop) (l : Rbar) :=
  forall x, E x -> Rbar_le l x.

Lemma Rbar_ub_lb (E : Rbar -> Prop) (l : Rbar) :
  Rbar_is_upper_bound (fun x => E (Rbar_opp x)) (Rbar_opp l)
    <-> Rbar_is_lower_bound E l.
Proof.
(* Goal: Rbar_le l b *)
  split => Hl x Hx.
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Rbar_opp_le.
(* Goal: Rbar_le (Rbar_opp l) (Rbar_opp x) *)
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Hl.
(* Goal: Rbar_le (Finite x) b *)
  by rewrite Rbar_opp_involutive.
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Rbar_opp_le.
(* Goal: @eq Rbar (Rbar_glb E) l *)
  rewrite Rbar_opp_involutive.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hl.
Qed.
Lemma Rbar_lb_ub (E : Rbar -> Prop) (l : Rbar) :
  Rbar_is_lower_bound (fun x => E (Rbar_opp x)) (Rbar_opp l)
    <-> Rbar_is_upper_bound E l.
Proof.
(* Goal: Rbar_le l b *)
  split => Hl x Hx.
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Rbar_opp_le.
(* Goal: Rbar_le (Rbar_opp l) (Rbar_opp x) *)
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Hl.
(* Goal: Rbar_le (Finite x) b *)
  by rewrite Rbar_opp_involutive.
(* Goal: Rbar_le (Rbar_opp l) x *)
  apply Rbar_opp_le.
(* Goal: @eq Rbar (Rbar_glb E) l *)
  rewrite Rbar_opp_involutive.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hl.
Qed.

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.
  split => [H x [<- Hx] | H x Hx] ; apply H => // ;
  by exists x.
Qed.
Lemma is_lb_Rbar_correct (E : R -> Prop) (l : Rbar) :
  is_lb_Rbar E l <-> Rbar_is_lower_bound (fun x => is_finite x /\ E x) l.
Proof.
  split => [H x [<- Hx] | H x Hx] ; apply H => // ;
  by exists x.
Qed.

(** Basic properties *)

Lemma Rbar_ub_p_infty (E : Rbar -> Prop) :
  Rbar_is_upper_bound E p_infty.
Proof.
(* Goal: Rbar_is_upper_bound E p_infty *)
  now intros [x| |] Hx.
Qed.
Lemma Rbar_lb_m_infty (E : Rbar -> Prop) :
  Rbar_is_lower_bound E m_infty.
Proof.
(* Goal: Rbar_is_lower_bound E m_infty *)
  easy.
Qed.

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.
(* Goal: forall _ : Rbar_is_lower_bound E (Finite l), is_upper_bound (fun x : R => E (Finite (Ropp x))) (Ropp l) *)
  intros H x Ex.
(* Goal: Rle x l *)
  now apply (H (Finite x)).
Qed.
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.
(* Goal: forall _ : Rbar_is_lower_bound E (Finite l), is_upper_bound (fun x : R => E (Finite (Ropp x))) (Ropp l) *)
  intros H x Ex.
  apply Ropp_le_cancel ; rewrite Ropp_involutive ;
  now apply (H (Finite (-x))).
Qed.

Lemma Rbar_ub_m_infty (E : Rbar -> Prop) :
  Rbar_is_upper_bound E m_infty -> forall x, E x -> x = m_infty.
Proof.
  intros H [x| |] Hx ;
  now specialize (H _ Hx).
Qed.
Lemma Rbar_lb_p_infty (E : Rbar -> Prop) :
  Rbar_is_lower_bound E p_infty -> (forall x, E x -> x = p_infty).
Proof.
  intros H x ;
  case x ; auto ; clear x ; [intros x| ] ; intros Hx.
(* Goal: @eq Rbar m_infty p_infty *)
  case (H _ Hx) ; simpl ; intuition.
(* Goal: @eq Rbar m_infty p_infty *)
  case (H _ Hx) ; simpl ; intuition.
Qed.

Lemma Rbar_lb_le_ub (E : Rbar -> Prop) (l1 l2 : Rbar) : (exists x, E x) ->
  Rbar_is_lower_bound E l1 -> Rbar_is_upper_bound E l2 -> Rbar_le l1 l2.
Proof.
  intros (x, Hex) Hl Hu ;
  apply Rbar_le_trans with (y := x) ; [apply Hl | apply Hu] ; auto.
Qed.
Lemma Rbar_lb_eq_ub (E : Rbar -> Prop) (l : Rbar) :
  Rbar_is_lower_bound E l -> Rbar_is_upper_bound E l -> forall x, E x -> x = l.
Proof.
(* Goal: forall (_ : Rbar_is_lower_bound E l) (_ : Rbar_is_upper_bound E l) (x : Rbar) (_ : E x), @eq Rbar x l *)
  intros Hl Hu x Hx.
(* Goal: @eq Rbar x l *)
  apply Rbar_le_antisym ; [apply Hu | apply Hl] ; auto.
Qed.

(** Decidability *)

Lemma Rbar_ub_dec (E : Rbar -> Prop) (Hp : ~ E p_infty) :
  {M : R | Rbar_is_upper_bound E M}
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    + {(forall (M : R), ~Rbar_is_upper_bound E M)}.
Proof.
(* Goal: sumor (@sig R (fun M : R => Rbar_is_upper_bound E (Finite M))) (forall M : R, not (Rbar_is_upper_bound E (Finite M))) *)
  destruct (is_ub_Rbar_dec E) as [ [M HM] | HM ].
(* Goal: sumor (@sig R (fun M : R => Rbar_is_upper_bound E (Finite M))) (forall M : R, not (Rbar_is_upper_bound E (Finite M))) *)
(* Goal: sumor (@sig R (fun M : R => Rbar_is_upper_bound E (Finite M))) (forall M : R, not (Rbar_is_upper_bound E (Finite M))) *)
  left ; exists M ; case => [x | | ] //= Hx.
(* Goal: Rbar_le (Finite x) b *)
  by apply HM.
(* Goal: Rbar_le l b *)
  right => M.
(* Goal: not (Rbar_is_upper_bound E (Finite M)) *)
  specialize (HM M).
(* Goal: Rbar_le l b *)
  contradict HM => x Hx.
(* Goal: Rbar_le (Finite x) b *)
  by apply HM.
Qed.
Lemma Rbar_lb_dec (E : Rbar -> Prop) (Hm : ~ E m_infty) :
  {M : R | Rbar_is_lower_bound E (Finite M)}
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
    + {(forall M, ~Rbar_is_lower_bound E (Finite M))}.
Proof.
(* Goal: sumor (@sig R (fun M : R => Rbar_is_lower_bound E (Finite M))) (forall M : R, not (Rbar_is_lower_bound E (Finite M))) *)
  destruct (Rbar_ub_dec (fun x => E (Rbar_opp x)) Hm) as [(M, H)|H].
(* Goal: sumor (@sig R (fun M : R => Rbar_is_lower_bound E (Finite M))) (forall M : R, not (Rbar_is_lower_bound E (Finite M))) *)
(* Goal: sumor (@sig R (fun M : R => Rbar_is_lower_bound E (Finite M))) (forall M : R, not (Rbar_is_lower_bound E (Finite M))) *)
  left ; exists (-M).
(* Goal: Rbar_is_lower_bound E (Finite (Ropp M)) *)
(* Goal: sumor (@sig R (fun M : R => Rbar_is_lower_bound E (Finite M))) (forall M : R, not (Rbar_is_lower_bound E (Finite M))) *)
  apply Rbar_ub_lb ; simpl ; rewrite (Ropp_involutive M) ; auto.
  right ; intro M ; generalize (H (-M)) ; clear H ; intro H ; contradict H ;
  apply (Rbar_ub_lb E (Finite M)) ; auto.
Qed.

(** Order *)

Lemma Rbar_is_ub_subset (E1 E2 : Rbar -> Prop) (l : Rbar) :
  (forall x, E1 x -> E2 x) -> (Rbar_is_upper_bound E2 l) -> (Rbar_is_upper_bound E1 l).
Proof.
(* Goal: forall (_ : forall (x : Rbar) (_ : E1 x), E2 x) (_ : Rbar_is_lower_bound E2 l), Rbar_is_lower_bound E1 l *)
  intros Hs Hl x Ex ; apply Hl, Hs ; auto.
Qed.
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.
(* Goal: forall (_ : forall (x : Rbar) (_ : E1 x), E2 x) (_ : Rbar_is_lower_bound E2 l), Rbar_is_lower_bound E1 l *)
  intros Hs Hl x Ex ; apply Hl, Hs ; auto.
Qed.

(** ** Least upper bound and Greatest Lower Bound *)

Definition Rbar_is_lub (E : Rbar -> Prop) (l : Rbar) :=
  Rbar_is_upper_bound E l /\
    (forall b : Rbar, Rbar_is_upper_bound E b -> Rbar_le l b).
Definition Rbar_is_glb (E : Rbar -> Prop) (l : Rbar) :=
  Rbar_is_lower_bound E l /\
    (forall b : Rbar, Rbar_is_lower_bound E b -> Rbar_le b l).

Lemma Rbar_lub_glb (E : Rbar -> Prop) (l : Rbar) :
  Rbar_is_lub (fun x => E (Rbar_opp x)) (Rbar_opp l)
    <-> Rbar_is_glb E l.
Proof.
(* Goal: is_lub_Rbar P (Finite x) *)
  split ; [intros (ub, lub) | intros (lb, glb)] ; split.
(* Goal: Rbar_is_lower_bound E l *)
(* Goal: forall (b : Rbar) (_ : Rbar_is_lower_bound E b), Rbar_le b l *)
(* Goal: Rbar_is_upper_bound (fun x : Rbar => E (Rbar_opp x)) (Rbar_opp l) *)
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound (fun x : Rbar => E (Rbar_opp x)) b), Rbar_le (Rbar_opp l) b *)
  apply Rbar_ub_lb ; auto.
(* Goal: Rbar_le (Rbar_opp l) x *)
  intros b Hb ; generalize (lub _ (proj2 (Rbar_ub_lb _ _) Hb)) ; apply Rbar_opp_le.
(* Goal: Rbar_is_upper_bound (fun x : Rbar => E (Rbar_opp x)) (Rbar_opp l) *)
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound (fun x : Rbar => E (Rbar_opp x)) b), Rbar_le (Rbar_opp l) b *)
  apply Rbar_lb_ub ; intros x ; simpl ; repeat rewrite Rbar_opp_involutive ; apply lb.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
  intros b Hb.
  apply Rbar_opp_le ; rewrite Rbar_opp_involutive ; apply glb, Rbar_ub_lb ;
  rewrite Rbar_opp_involutive ; auto.
Qed.
Lemma Rbar_glb_lub (E : Rbar -> Prop) (l : Rbar) :
  Rbar_is_glb (fun x => E (Rbar_opp x)) (Rbar_opp l)
    <-> Rbar_is_lub E l.
Proof.
(* Goal: is_lub_Rbar P (Finite x) *)
  split ; [ intros (lb, glb) | intros (ub, lub)] ; split.
(* Goal: Rbar_is_upper_bound E l *)
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
(* Goal: Rbar_is_lower_bound (fun x : Rbar => E (Rbar_opp x)) (Rbar_opp l) *)
(* Goal: forall (b : Rbar) (_ : Rbar_is_lower_bound (fun x : Rbar => E (Rbar_opp x)) b), Rbar_le b (Rbar_opp l) *)
  apply Rbar_lb_ub ; auto.
(* Goal: Rbar_le (Rbar_opp l) x *)
  intros b Hb ; generalize (glb _ (proj2 (Rbar_lb_ub _ _) Hb)) ; apply Rbar_opp_le.
(* Goal: Rbar_is_lower_bound (fun x : Rbar => E (Rbar_opp x)) (Rbar_opp l) *)
(* Goal: forall (b : Rbar) (_ : Rbar_is_lower_bound (fun x : Rbar => E (Rbar_opp x)) b), Rbar_le b (Rbar_opp l) *)
  apply Rbar_ub_lb ; intro x ; simpl ; repeat rewrite Rbar_opp_involutive ; apply ub.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
  intros b Hb.
  apply Rbar_opp_le ; rewrite Rbar_opp_involutive ; apply lub, Rbar_lb_ub ;
  rewrite Rbar_opp_involutive ; auto.
Qed.

Lemma is_lub_Rbar_correct (E : R -> Prop) (l : Rbar) :
  is_lub_Rbar E l <-> Rbar_is_lub (fun x => is_finite x /\ E x) l.
Proof.
(* Goal: Rbar_le l b *)
  split => [[Hub Hlub]|[Hub Hlub]].
(* Goal: is_glb_Rbar E l *)
  split ; [ | move => b Hb ; apply Hlub ] ; by apply is_ub_Rbar_correct.
(* Goal: is_glb_Rbar E l *)
  split ; [ | move => b Hb ; apply Hlub ] ; by apply is_ub_Rbar_correct.
Qed.
Lemma is_glb_Rbar_correct (E : R -> Prop) (l : Rbar) :
  is_glb_Rbar E l <-> Rbar_is_glb (fun x => is_finite x /\ E x) l.
Proof.
(* Goal: Rbar_le l b *)
  split => [[Hub Hlub]|[Hub Hlub]].
(* Goal: is_glb_Rbar E l *)
  split ; [ | move => b Hb ; apply Hlub ] ; by apply is_lb_Rbar_correct.
(* Goal: is_glb_Rbar E l *)
  split ; [ | move => b Hb ; apply Hlub ] ; by apply is_lb_Rbar_correct.
Qed.

Lemma Rbar_ex_lub (E : Rbar -> Prop) :
  {l : Rbar | Rbar_is_lub E l}.
Proof.
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_lub E l) *)
  destruct (EM_dec (E p_infty)) as [Hp|Hp].
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_lub E l) *)
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_lub E l) *)
  exists p_infty ; split.
(* Goal: Rbar_le (Finite x) b *)
  by case.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
  intros b Hb.
(* Goal: Rbar_le p_infty b *)
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_lub E l) *)
  apply Rbar_not_lt_le.
(* Goal: Rbar_le l b *)
  contradict Hp => H.
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_lub E l) *)
  apply: Rbar_le_not_lt Hp.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hb.
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_lub E l) *)
  destruct (ex_lub_Rbar E) as [l Hl].
(* Goal: is_lub_Rbar P (Finite x) *)
  exists l ; split.
  case => [x | | ] // Hx.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hl.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E b), Rbar_le l b *)
  intros b Hb.
(* Goal: Rbar_le l b *)
  apply Hl => x Hx.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hb.
Qed.

Lemma Rbar_ex_glb (E : Rbar -> Prop) :
  {l : Rbar | Rbar_is_glb E l}.
Proof.
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_glb E l) *)
  destruct (Rbar_ex_lub (fun x => E (Rbar_opp x))) as [l Hl].
(* Goal: @sig Rbar (fun l : Rbar => Rbar_is_glb E l) *)
  exists (Rbar_opp l).
(* Goal: @eq Rbar (Rbar_glb E) l *)
  now apply Rbar_lub_glb ; rewrite Rbar_opp_involutive.
Qed.

(** Functions *)

Definition Rbar_lub (E : Rbar -> Prop)
  := proj1_sig (Rbar_ex_lub E).
Definition Rbar_glb (E : Rbar -> Prop)
  := proj1_sig (Rbar_ex_glb E).

Lemma Rbar_opp_glb_lub (E : Rbar -> Prop) :
  Rbar_glb (fun x => E (Rbar_opp x)) = Rbar_opp (Rbar_lub E).
Proof.
  unfold Rbar_glb ; case (Rbar_ex_glb _) ; simpl ; intros g [Hg Hg'] ;
  unfold Rbar_lub ; case (Rbar_ex_lub _) ; simpl ; intros l [Hl Hl'] ;
(* Goal: @eq Rbar l0 l *)
  apply Rbar_le_antisym.
  apply Rbar_opp_le ; rewrite Rbar_opp_involutive ; apply Hl', Rbar_lb_ub ;
  rewrite Rbar_opp_involutive ; auto.
(* Goal: Rbar_le (Rbar_opp l) g *)
  apply Hg', Rbar_lb_ub ; auto.
Qed.
Lemma Rbar_opp_lub_glb (E : Rbar -> Prop) :
  Rbar_lub (fun x => E (Rbar_opp x)) = Rbar_opp (Rbar_glb E).
Proof.
  unfold Rbar_glb ; case (Rbar_ex_glb _) ; simpl ; intros g (Hg, Hg') ;
  unfold Rbar_lub ; case (Rbar_ex_lub _) ; simpl ; intros l [Hl Hl'] ;
(* Goal: @eq Rbar l0 l *)
  apply Rbar_le_antisym.
  apply Hl', Rbar_lb_ub ; rewrite Rbar_opp_involutive ;
  apply (Rbar_is_lb_subset _ E) ; auto ; intros x ; rewrite Rbar_opp_involutive ; auto.
  apply Rbar_opp_le ; rewrite Rbar_opp_involutive ; apply Hg', Rbar_ub_lb ;
  rewrite Rbar_opp_involutive ; auto.
Qed.

Lemma Rbar_is_lub_unique (E : Rbar -> Prop) (l : Rbar) :
  Rbar_is_lub E l -> Rbar_lub E = l.
Proof.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => H.
(* Goal: @eq Rbar (Rbar_glb E) l *)
  rewrite /Rbar_lub.
(* Goal: P (real (Lub_Rbar P)) *)
  case: Rbar_ex_lub => l0 H0 /=.
(* Goal: @eq Rbar l0 l *)
  apply Rbar_le_antisym.
(* Goal: Rbar_le l l0 *)
  apply H0, H.
(* Goal: Rbar_le l0 l *)
(* Goal: Rbar_le l l0 *)
  apply H, H0.
Qed.
Lemma Rbar_is_glb_unique (E : Rbar -> Prop) (l : Rbar) :
  Rbar_is_glb E l -> Rbar_glb E = l.
Proof.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => H.
(* Goal: @eq Rbar (Rbar_glb E) l *)
  rewrite /Rbar_glb.
(* Goal: P (real (Lub_Rbar P)) *)
  case: Rbar_ex_glb => l0 H0 /=.
(* Goal: @eq Rbar l0 l *)
  apply Rbar_le_antisym.
(* Goal: Rbar_le l0 l *)
(* Goal: Rbar_le l l0 *)
  apply H, H0.
(* Goal: Rbar_le l l0 *)
  apply H0, H.
Qed.

(** Order *)

Lemma Rbar_glb_le_lub (E : Rbar -> Prop) :
  (exists x, E x) -> Rbar_le (Rbar_glb E) (Rbar_lub E).
Proof.
(* Goal: P (real (Lub_Rbar P)) *)
  case => x Hex.
(* Goal: Rbar_le (Rbar_glb E) (Rbar_lub E) *)
  apply Rbar_le_trans with x.
(* Goal: Rbar_le (Rbar_glb E) x *)
(* Goal: Rbar_le x (Rbar_lub E) *)
  unfold Rbar_glb ; case (Rbar_ex_glb _) ; simpl ; intros g (Hg, _) ; apply Hg ; auto.
(* Goal: Rbar_le x (Rbar_lub E) *)
  unfold Rbar_lub ; case (Rbar_ex_lub _) ; simpl ; intros l (Hl, _) ; apply Hl ; auto.
Qed.

Lemma Rbar_is_lub_subset (E1 E2 : Rbar -> Prop) (l1 l2 : Rbar) :
  (forall x, E1 x -> E2 x) -> (Rbar_is_lub E1 l1) -> (Rbar_is_lub E2 l2)
  -> Rbar_le l1 l2.
Proof.
(* Goal: forall (_ : forall (x : Rbar) (_ : E1 x), E2 x) (_ : Rbar_is_lub E1 l1) (_ : Rbar_is_lub E2 l2), Rbar_le l1 l2 *)
  intros Hs (_,H1) (H2, _).
(* Goal: Rbar_le l1 l2 *)
  apply H1 ; intros x Hx ; apply H2, Hs, Hx.
Qed.
Lemma Rbar_is_glb_subset (E1 E2 : Rbar -> Prop) (l1 l2 : Rbar) :
  (forall x, E2 x -> E1 x) -> (Rbar_is_glb E1 l1) -> (Rbar_is_glb E2 l2)
  -> Rbar_le l1 l2.
Proof.
(* Goal: forall (_ : forall (x : Rbar) (_ : E2 x), E1 x) (_ : Rbar_is_glb E1 l1) (_ : Rbar_is_glb E2 l2), Rbar_le l1 l2 *)
  intros Hs (H1, _) (_, H2).
(* Goal: Rbar_le l1 l2 *)
  apply H2 ; intros x Hx ; apply H1, Hs, Hx.
Qed.

Lemma Rbar_is_lub_eq (E1 E2 : Rbar -> Prop) (l1 l2 : Rbar) :
  (forall x, E1 x <-> E2 x) -> (Rbar_is_lub E1 l1) -> (Rbar_is_lub E2 l2)
  -> l1 = l2.
Proof.
  intros Hs H1 H2 ; apply Rbar_le_antisym ;
  [apply (Rbar_is_lub_subset E1 E2) | apply (Rbar_is_lub_subset E2 E1) ] ; auto ; intros x H ;
  apply Hs ; auto.
Qed.
Lemma Rbar_is_glb_eq (E1 E2 : Rbar -> Prop) (l1 l2 : Rbar) :
  (forall x, E1 x <-> E2 x) -> (Rbar_is_glb E1 l1) -> (Rbar_is_glb E2 l2)
  -> l1 = l2.
Proof.
  intros Hs H1 H2 ; apply Rbar_le_antisym ;
  [apply (Rbar_is_glb_subset E1 E2) | apply (Rbar_is_glb_subset E2 E1) ] ; auto ; intros x H ;
  apply Hs ; auto.
Qed.

Lemma Rbar_is_lub_ext (E1 E2 : Rbar -> Prop) (l : Rbar) :
  (forall x, E1 x <-> E2 x) -> (Rbar_is_lub E1 l) -> (Rbar_is_lub E2 l).
Proof.
(* Goal: is_lub_Rbar P (Finite x) *)
  intros Heq (H1,H2) ; split.
(* Goal: Rbar_is_upper_bound E2 l *)
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E2 b), Rbar_le l b *)
  apply (Rbar_is_ub_subset _ E1) ; auto ; intros x Hx ; apply Heq ; auto.
(* Goal: forall (b : Rbar) (_ : Rbar_is_upper_bound E2 b), Rbar_le l b *)
  intros b Hb ; apply H2 ; apply (Rbar_is_ub_subset _ E2) ; auto ; intros x Hx ; apply Heq ; auto.
Qed.
Lemma Rbar_is_glb_ext (E1 E2 : Rbar -> Prop) (l : Rbar) :
  (forall x, E1 x <-> E2 x) -> (Rbar_is_glb E1 l) -> (Rbar_is_glb E2 l).
Proof.
(* Goal: is_lub_Rbar P (Finite x) *)
  intros Heq (H1, H2) ; split.
(* Goal: Rbar_is_lower_bound E2 l *)
(* Goal: forall (b : Rbar) (_ : Rbar_is_lower_bound E2 b), Rbar_le b l *)
  apply (Rbar_is_lb_subset _ E1) ; auto ; intros x Hx ; apply Heq ; auto.
(* Goal: forall (b : Rbar) (_ : Rbar_is_lower_bound E2 b), Rbar_le b l *)
  intros b Hb ; apply H2 ; apply (Rbar_is_lb_subset _ E2) ; auto ; intros x Hx ; apply Heq ; auto.
Qed.

Lemma Rbar_lub_subset (E1 E2 : Rbar -> Prop) :
  (forall x, E1 x -> E2 x) -> Rbar_le (Rbar_lub E1) (Rbar_lub E2).
Proof.
  intros Hs ; unfold Rbar_lub ; case (Rbar_ex_lub E1) ; intros l1 Hl1 ;
  case (Rbar_ex_lub E2) ; simpl ; intros l2 Hl2 ; apply (Rbar_is_lub_subset E1 E2) ; auto.
Qed.
Lemma Rbar_glb_subset (E1 E2 : Rbar -> Prop) :
  (forall x, E2 x -> E1 x) -> Rbar_le (Rbar_glb E1) (Rbar_glb E2).
Proof.
  intro Hs ; unfold Rbar_glb ; case (Rbar_ex_glb E1) ; intros l1 Hl1 ;
  case (Rbar_ex_glb E2) ; simpl ; intros l2 Hl2 ; apply (Rbar_is_glb_subset E1 E2) ; auto.
Qed.

Lemma Rbar_lub_rw (E1 E2 : Rbar -> Prop) :
  (forall x, E1 x <-> E2 x) -> Rbar_lub E1 = Rbar_lub E2.
Proof.
(* Goal: forall _ : forall x : Rbar, iff (E1 x) (E2 x), @eq Rbar (Rbar_lub E1) (Rbar_lub E2) *)
  intro Hs ; apply Rbar_le_antisym ; apply Rbar_lub_subset ; intros x H ; apply Hs ; auto.
Qed.
Lemma Rbar_glb_rw (E1 E2 : Rbar -> Prop) :
  (forall x, E1 x <-> E2 x) -> Rbar_glb E1 = Rbar_glb E2.
Proof.
(* Goal: forall _ : forall x : Rbar, iff (E1 x) (E2 x), @eq Rbar (Rbar_glb E1) (Rbar_glb E2) *)
  intros Hs ; apply Rbar_le_antisym ; apply Rbar_glb_subset ; intros x H ; apply Hs ; auto.
Qed.

(** * Emptiness is decidable *)

Definition Empty (E : R -> Prop) :=
  Lub_Rbar (fun x => x = 0 \/ E x) = Glb_Rbar (fun x => x = 0 \/ E x)
  /\ Lub_Rbar (fun x => x = 1 \/ E x) = Glb_Rbar (fun x => x = 1 \/ E x).

Lemma Empty_correct_1 (E : R -> Prop) :
  Empty E -> forall x, ~ E x.
Proof.
(* Goal: P (real (Lub_Rbar P)) *)
  case => E0 E1 x Ex.
  rewrite /Lub_Rbar /Glb_Rbar in E0 ;
  case : (ex_lub_Rbar (fun x : R => x = 0 \/ E x)) E0 => /= s0 Hs0 ;
  case : (ex_glb_Rbar (fun x : R => x = 0 \/ E x)) => i0 Hi0 /= E0.
(* Goal: forall _ : @eq R x (IZR Z0), False *)
  have : (x = 0) ; last move => {s0 Hs0 i0 Hi0 E0}.
(* Goal: @eq R x (IZR (Zpos xH)) *)
(* Goal: forall (_ : @eq R x (IZR (Zpos xH))) (_ : @eq R x (IZR Z0)), False *)
  apply Rle_antisym.
(* Goal: Rle x (IZR Z0) *)
(* Goal: Rle (IZR Z0) x *)
(* Goal: forall _ : @eq R x (IZR Z0), False *)
  apply (Rbar_le_trans x s0 0).
(* Goal: Rbar_le (Finite x) b *)
  apply Hs0 ; by right.
(* Goal: Rbar_le (Finite x) b *)
  rewrite E0 ; apply Hi0 ; by left.
(* Goal: Rle (IZR Z0) x *)
(* Goal: forall _ : @eq R x (IZR Z0), False *)
  apply (Rbar_le_trans 0 s0 x).
(* Goal: Rbar_le (Finite x) b *)
  apply Hs0 ; by left.
(* Goal: Rbar_le (Finite x) b *)
  rewrite E0 ; apply Hi0 ; by right.
  rewrite /Lub_Rbar /Glb_Rbar in E1 ;
  case : (ex_lub_Rbar (fun x : R => x = 1 \/ E x)) E1 => /= s1 Hs1 ;
  case : (ex_glb_Rbar (fun x : R => x = 1 \/ E x)) => i1 Hi1 /= E1.
(* Goal: forall _ : @eq R x (IZR Z0), False *)
  have : (x = 1) ; last move => {s1 Hs1 i1 Hi1 E1}.
(* Goal: @eq R x (IZR (Zpos xH)) *)
(* Goal: forall (_ : @eq R x (IZR (Zpos xH))) (_ : @eq R x (IZR Z0)), False *)
  apply Rle_antisym.
(* Goal: Rle x (IZR (Zpos xH)) *)
(* Goal: Rle (IZR (Zpos xH)) x *)
(* Goal: forall (_ : @eq R x (IZR (Zpos xH))) (_ : @eq R x (IZR Z0)), False *)
  apply (Rbar_le_trans x s1 1).
(* Goal: Rbar_le (Finite x) b *)
  apply Hs1 ; by right.
(* Goal: Rbar_le (Finite x) b *)
  rewrite E1 ; apply Hi1 ; by left.
(* Goal: Rle (IZR (Zpos xH)) x *)
(* Goal: forall (_ : @eq R x (IZR (Zpos xH))) (_ : @eq R x (IZR Z0)), False *)
  apply (Rbar_le_trans 1 s1 x).
(* Goal: Rbar_le (Finite x) b *)
  apply Hs1 ; by left.
(* Goal: Rbar_le (Finite x) b *)
  rewrite E1 ; apply Hi1 ; by right.
(* Goal: forall (_ : @eq R x (IZR (Zpos xH))) (_ : @eq R x (IZR Z0)), False *)
  move => -> ; apply R1_neq_R0.
Qed.

Lemma Empty_correct_2 (E : R -> Prop) :
  (forall x, ~ E x) -> Empty E.
Proof.
  move => H ; split ;
  rewrite /Glb_Rbar /Lub_Rbar ;
  [ case : (ex_lub_Rbar (fun x : R => x = 0 \/ E x)) => s0 Hs0 ;
  case : (ex_glb_Rbar (fun x : R => x = 0 \/ E x)) => i0 Hi0 /=
  | case : (ex_lub_Rbar (fun x : R => x = 1 \/ E x)) => s1 Hs1 ;
  case : (ex_glb_Rbar (fun x : R => x = 1 \/ E x)) => i1 Hi1 /=].
  have : (i0 = Finite 0) ; last move => -> ;
  apply: Rbar_le_antisym.
(* Goal: Rbar_le (Finite x) b *)
  apply Hi0 ; by left.
(* Goal: bound (E m) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  apply Hi0 => y ; case => H0.
(* Goal: Rbar_le (Finite x) b *)
  rewrite H0 ; by right.
  contradict H0 ; apply H.
(* Goal: bound (E m) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  apply Hs0 => y ; case => H0.
(* Goal: Rbar_le (Finite x) b *)
  rewrite H0 ; by right.
  contradict H0 ; apply H.
(* Goal: Rbar_le (Finite x) b *)
  apply Hs0 ; by left.
  have : (i1 = Finite 1) ; last move => -> ;
  apply: Rbar_le_antisym.
(* Goal: Rbar_le (Finite x) b *)
  apply Hi1 ; by left.
(* Goal: bound (E m) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  apply Hi1 => y ; case => H1.
(* Goal: Rbar_le (Finite x) b *)
  rewrite H1 ; by right.
  contradict H1 ; apply H.
(* Goal: bound (E m) *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  apply Hs1 => y ; case => H1.
(* Goal: Rbar_le (Finite x) b *)
  rewrite H1 ; by right.
  contradict H1 ; apply H.
(* Goal: Rbar_le (Finite x) b *)
  apply Hs1 ; by left.
Qed.

Lemma Empty_dec (E : R -> Prop) :
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  {~Empty E}+{Empty E}.
Proof.
  case: (Rbar_eq_dec (Lub_Rbar (fun x => x = 0 \/ E x)) (Glb_Rbar (fun x => x = 0 \/ E x))) => H0 ;
    [ | left].
  case: (Rbar_eq_dec (Lub_Rbar (fun x => x = 1 \/ E x)) (Glb_Rbar (fun x => x = 1 \/ E x))) => H1 ;
    [by right | left].
(* Goal: not (Empty E) *)
(* Goal: not (Empty E) *)
  contradict H1 ; apply H1.
(* Goal: not (Empty E) *)
  contradict H0 ; apply H0.
Qed.
Lemma not_Empty_dec (E : R -> Prop) : (Decidable.decidable (exists x, E x)) ->
(* Goal: False *)
(* Goal: @sig Rbar (fun l : Rbar => is_lub_Rbar F l) *)
  {(exists x, E x)} + {(forall x, ~ E x)}.
Proof.
  move => He ;
  case: (Empty_dec E) => Hx ;
  [left|right].
(* Goal: P (real (Lub_Rbar P)) *)
  case: He => // He.
  contradict Hx ;
  apply: Empty_correct_2 => x ; contradict He ; by exists x.
(* Goal: Rbar_le (Finite x) b *)
  by apply: Empty_correct_1.
Qed.

Lemma uniqueness_dec P : (exists ! x : R, P x) -> {x : R | P x}.
Proof.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => H.
(* Goal: @sig R (fun x : R => P x) *)
  exists (Lub_Rbar P).
(* Goal: P (real (Lub_Rbar P)) *)
  case: H => x Hx.
(* Goal: P (real (Lub_Rbar P)) *)
  replace (real (Lub_Rbar P)) with (real (Finite x)).
(* Goal: Rbar_le (Finite x) b *)
  by apply Hx.
(* Goal: @eq R (real (Finite x)) (real (Lub_Rbar P)) *)
  apply f_equal, sym_eq, is_lub_Rbar_unique.
(* Goal: is_lub_Rbar P (Finite x) *)
  split.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => y Hy.
(* Goal: Rbar_le (Finite y) (Finite x) *)
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  right ; by apply sym_eq, Hx.
(* Goal: forall (b : Rbar) (_ : is_ub_Rbar P b), Rbar_le (Finite x) b *)
  move => b Hb.
(* Goal: Rbar_le (Finite x) b *)
  by apply Hb, Hx.
Qed.
