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

(* Goal: sumbool P (not P) *)
Copyright (C) 2011-2015 Sylvie Boldo
#<br />#
(* Goal: sumbool P (not P) *)
Copyright (C) 2011-2015 Catherine Lelay
#<br />#
(* Goal: sumbool P (not P) *)
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 RIneq Rcomplements Omega.

(** This file proves the Limited Principle of Omniscience: given a
decidable property P on [nat], either P never holds or we can construct
a witness for which P holds. Several variants are given. *)

Open Scope R_scope.

(** * Limited Principle of Omniscience *)

Theorem LPO_min :
(* Goal: sumbool P (not P) *)
  forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
(* Goal: sumbool P (not P) *)
  {n : nat | P n /\ forall i, (i < n)%nat -> ~ P i} + {forall n, ~ P n}.
Proof.
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
assert (Hi: forall n, 0 < INR n + 1).
(* Goal: forall n : nat, Rlt (IZR Z0) (Rplus (INR n) (IZR (Zpos xH))) *)
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  intros N.
(* Goal: Rle (IZR (Zpos xH)) (Rplus (INR i) (IZR (Zpos xH))) *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite <- S_INR.
(* Goal: Rlt (IZR Z0) (INR (S N)) *)
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply lt_0_INR.
(* Goal: lt O (S N) *)
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply lt_0_Sn.
(* Goal: forall (P : Prop) (_ : or P (not P)), sumbool P (not P) *)
intros P HP.
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
set (E y := exists n, (P n /\ y = / (INR n + 1)) \/ (~ P n /\ y = 0)).
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
assert (HE: forall n, P n -> E (/ (INR n + 1))).
(* Goal: forall n : nat, not (P n) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  intros n Pn.
(* Goal: E (Rinv (Rplus (INR n) (IZR (Zpos xH)))) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exists n.
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
  left.
(* Goal: and (@eq R (IZR (Zpos xH)) (IZR (Zpos xH))) P *)
  now split.
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
assert (BE: is_upper_bound E 1).
(* Goal: is_upper_bound E (IZR (Zpos xH)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  intros x [y [[_ ->]|[_ ->]]].
(* Goal: Rle (Rinv (Rplus (INR y) (IZR (Zpos xH)))) (IZR (Zpos xH)) *)
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  rewrite <- Rinv_1 at 2.
(* Goal: Rle (Rinv (IZR (Zpos xH))) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
  apply Rinv_le_contravar.
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: Rle (IZR (Zpos xH)) (Rplus (INR y) (IZR (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exact Rlt_0_1.
(* Goal: Rle (IZR (Zpos xH)) (Rplus (INR i) (IZR (Zpos xH))) *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite <- S_INR.
(* Goal: Rle (IZR (Zpos xH)) (INR (S y)) *)
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply (le_INR 1), le_n_S, le_0_n.
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exact Rle_0_1.
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
destruct (completeness E) as [l [ub lub]].
(* Goal: bound E *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  now exists 1.
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  destruct (HP O) as [H0|H0].
(* Goal: bound E *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumbool (not (not P)) (not P) *)
  exists 1.
(* Goal: E (IZR Z0) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exists O.
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
  left.
(* Goal: and (P O) (@eq R (IZR (Zpos xH)) (Rinv (Rplus (INR O) (IZR (Zpos xH))))) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply (conj H0).
(* Goal: @eq R (IZR (Zpos xH)) (Rinv (Rplus (INR O) (IZR (Zpos xH)))) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  rewrite Rplus_0_l.
(* Goal: @eq R (IZR (Zpos xH)) (Rinv (IZR (Zpos xH))) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply sym_eq, Rinv_1.
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumbool (not (not P)) (not P) *)
  exists 0.
(* Goal: E (IZR Z0) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exists O.
(* Goal: E (IZR (Zpos xH)) *)
  right.
(* Goal: and (@eq R (IZR (Zpos xH)) (IZR (Zpos xH))) P *)
  now split.
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
destruct (Rle_lt_dec l 0) as [Hl|Hl].
(* Goal: E (IZR (Zpos xH)) *)
  right.
(* Goal: forall n : nat, not (P n) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  intros n Pn.
(* Goal: False *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply Rle_not_lt with (1 := Hl).
(* Goal: Rlt (IZR Z0) l *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply Rlt_le_trans with (/ (INR n + 1)).
(* Goal: Rlt (IZR Z0) (Rinv (Rplus (INR n) (IZR (Zpos xH)))) *)
(* Goal: Rle (Rinv (Rplus (INR n) (IZR (Zpos xH)))) l *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  now apply Rinv_0_lt_compat.
(* Goal: Rle (Rinv (Rplus (INR n) (IZR (Zpos xH)))) l *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply ub.
(* Goal: E (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: Rlt l (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  now apply HE.
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
left.
(* Goal: @sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i))) *)
set (N := Zabs_nat (up (/l) - 2)).
(* Goal: @sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i))) *)
exists N.
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
assert (HN: INR N + 1 = IZR (up (/ l)) - 1).
(* Goal: @eq R (Rplus (INR N) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  unfold N.
(* Goal: @eq R (Rplus (INR (Z.abs_nat (Z.sub (up (Rinv l)) (Zpos (xO xH))))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite INR_IZR_INZ.
(* Goal: @eq R (Rplus (IZR (Z.of_nat (Z.abs_nat (Z.sub (up (Rinv l)) (Zpos (xO xH)))))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite inj_Zabs_nat.
(* Goal: @eq R (Rplus (IZR (Z.abs (Z.sub (up (Rinv l)) (Zpos (xO xH))))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  replace (IZR (up (/ l)) - 1) with (IZR (up (/ l) - 2) + 1).
(* Goal: @eq R (Rplus (IZR (Z.abs (Z.sub (up (Rinv l)) (Zpos (xO xH))))) (IZR (Zpos xH))) (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply (f_equal (fun v => IZR v + 1)).
(* Goal: @eq Z (Z.abs (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (Z.sub (up (Rinv l)) (Zpos (xO xH))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Zabs_eq.
(* Goal: Z.le Z0 (Z.sub (up (Rinv l)) (Zpos (xO xH))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Zle_minus_le_0.
(* Goal: Z.le (Zpos (xO xH)) (up (Rinv l)) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply (Zlt_le_succ 1).
(* Goal: Z.lt (Zpos xH) (up (Rinv l)) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply lt_IZR.
(* Goal: Rlt (IZR (Zpos xH)) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Rle_lt_trans with (/l).
(* Goal: Rle (IZR (Zpos xH)) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Rmult_le_reg_r with (1 := Hl).
(* Goal: Rle (Rmult (IZR (Zpos xH)) l) (Rmult (Rinv l) l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite Rmult_1_l, Rinv_l by now apply Rgt_not_eq.
(* Goal: Rle l (IZR (Zpos xH)) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply lub.
(* Goal: is_upper_bound E (IZR (Zpos xH)) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  exact BE.
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
  apply archimed.
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite minus_IZR.
(* Goal: forall n : nat, or (@eq bool (f n) true) (not (@eq bool (f n) true)) *)
(* Goal: sumor (@sig nat (fun n : nat => @eq bool (f n) true)) (forall n : nat, @eq bool (f n) false) *)
(* Goal: sumor (@sig nat (fun n : nat => @eq bool (f n) true)) (forall n : nat, @eq bool (f n) false) *)
  simpl.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  ring.
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
assert (H: forall i, (i < N)%nat -> ~ P i).
(* Goal: forall (i : nat) (_ : lt i N), not (P i) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  intros i HiN Pi.
(* Goal: False *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  unfold is_upper_bound in ub.
(* Goal: False *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  refine (Rle_not_lt _ _ (ub (/ (INR i + 1)) _) _).
(* Goal: E (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: Rlt l (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  now apply HE.
(* Goal: Rlt l (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq.
(* Goal: Rlt (Rinv (IZR (up (Rinv l)))) (Rinv (Rinv l)) *)
  apply Rinv_1_lt_contravar.
(* Goal: Rle (IZR (Zpos xH)) (Rplus (INR i) (IZR (Zpos xH))) *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite <- S_INR.
(* Goal: Rle (IZR (Zpos xH)) (INR (S i)) *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply (le_INR 1).
(* Goal: le (S O) (S i) *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply le_n_S.
(* Goal: le O i *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply le_0_n.
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Rlt_le_trans with (INR N + 1).
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rplus (INR N) (IZR (Zpos xH))) *)
(* Goal: Rle (Rplus (INR N) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Rplus_lt_compat_r.
(* Goal: Rlt (INR i) (INR N) *)
(* Goal: Rle (Rplus (INR N) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  now apply lt_INR.
(* Goal: Rle (Rplus (INR N) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite HN.
(* Goal: Rle (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Rplus_le_reg_r with (-/l + 1).
(* Goal: Rle (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) (Rplus (Ropp (Rinv l)) (IZR (Zpos xH)))) (Rplus (Rinv l) (Rplus (Ropp (Rinv l)) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  ring_simplify.
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
  apply archimed.
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct (HP N) as [PN|PN].
(* Goal: and (@eq R (IZR (Zpos xH)) (IZR (Zpos xH))) P *)
  now split.
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
elimtype False.
(* Goal: False *)
refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1)) _) _).
(* Goal: is_upper_bound E (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  intros x [y [[Py ->]|[_ ->]]].
(* Goal: Rle (Rinv (Rplus (INR y) (IZR (Zpos xH)))) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  destruct (eq_nat_dec y N) as [HyN|HyN].
(* Goal: Rle (Rinv (Rplus (INR y) (IZR (Zpos xH)))) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rle (Rinv (Rplus (INR y) (IZR (Zpos xH)))) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  elim PN.
(* Goal: P N *)
(* Goal: Rle (Rinv (Rplus (INR y) (IZR (Zpos xH)))) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  now rewrite <- HyN.
(* Goal: Rle (Rinv (IZR (Zpos xH))) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
  apply Rinv_le_contravar.
(* Goal: Rlt (IZR Z0) (Rplus (INR (S N)) (IZR (Zpos xH))) *)
(* Goal: Rle (Rplus (INR (S N)) (IZR (Zpos xH))) (Rplus (INR y) (IZR (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  apply Hi.
(* Goal: Rle (Rplus (INR (S N)) (IZR (Zpos xH))) (Rplus (INR y) (IZR (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  apply Rplus_le_compat_r.
(* Goal: Rle (INR (S N)) (INR y) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  apply Rnot_lt_le.
(* Goal: not (Rlt (INR y) (INR (S N))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  intros Hy.
(* Goal: False *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  refine (H _ _ Py).
(* Goal: lt y N *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  apply INR_lt in Hy.
(* Goal: lt y N *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  clear -Hy HyN.
(* Goal: lt y N *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  omega.
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  now apply Rlt_le, Rinv_0_lt_compat.
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
rewrite S_INR, HN.
(* Goal: Rlt (Rinv (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) (IZR (Zpos xH)))) l *)
ring_simplify (IZR (up (/ l)) - 1 + 1).
(* Goal: Rlt (Rinv (IZR (up (Rinv l)))) l *)
rewrite <- (Rinv_involutive l) at 2 by now apply Rgt_not_eq.
(* Goal: Rlt (Rinv (IZR (up (Rinv l)))) (Rinv (Rinv l)) *)
apply Rinv_1_lt_contravar.
(* Goal: Rle (IZR (Zpos xH)) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
rewrite <- Rinv_1.
(* Goal: Rle (Rinv (IZR (Zpos xH))) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
apply Rinv_le_contravar.
(* Goal: Rlt (IZR Z0) l *)
(* Goal: Rle l (IZR (Zpos xH)) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
exact Hl.
(* Goal: Rle l (IZR (Zpos xH)) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
now apply lub.
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
apply archimed.
Qed.

Theorem LPO :
(* Goal: sumbool P (not P) *)
  forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
  {n : nat | P n} + {forall n, ~ P n}.
Proof.
(* Goal: forall (P : Prop) (_ : or P (not P)), sumbool P (not P) *)
intros P HP.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
destruct (LPO_min P HP) as [[n [Pn _]]|Pn].
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
left.
(* Goal: E (Rinv (Rplus (INR n) (IZR (Zpos xH)))) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
now exists n.
(* Goal: E (IZR (Zpos xH)) *)
now right.
Qed.

Lemma LPO_bool :
(* Goal: sumbool P (not P) *)
  forall f : nat -> bool,
  {n | f n = true} + {forall n, f n = false}.
Proof.
(* Goal: forall f : forall _ : nat, bool, sumor (@sig nat (fun n : nat => @eq bool (f n) true)) (forall n : nat, @eq bool (f n) false) *)
intros f.
(* Goal: sumor (@sig nat (fun n : nat => @eq bool (f n) true)) (forall n : nat, @eq bool (f n) false) *)
destruct (LPO (fun n => f n = true)) as [H|H].
(* Goal: forall n : nat, or (@eq bool (f n) true) (not (@eq bool (f n) true)) *)
(* Goal: sumor (@sig nat (fun n : nat => @eq bool (f n) true)) (forall n : nat, @eq bool (f n) false) *)
(* Goal: sumor (@sig nat (fun n : nat => @eq bool (f n) true)) (forall n : nat, @eq bool (f n) false) *)
simpl.
(* Goal: forall n : nat, or (Rlt M (u n)) (not (Rlt M (u n))) *)
(* Goal: not (forall n : nat, not (Rlt M (u n))) *)
intros n.
(* Goal: or (@eq bool (f n) true) (not (@eq bool (f n) true)) *)
(* Goal: sumor (@sig nat (fun n : nat => @eq bool (f n) true)) (forall n : nat, @eq bool (f n) false) *)
(* Goal: sumor (@sig nat (fun n : nat => @eq bool (f n) true)) (forall n : nat, @eq bool (f n) false) *)
case (f n).
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
now left.
(* Goal: E (IZR (Zpos xH)) *)
now right.
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
now left.
(* Goal: E (IZR (Zpos xH)) *)
right.
(* Goal: forall n : nat, or (Rlt M (u n)) (not (Rlt M (u n))) *)
(* Goal: not (forall n : nat, not (Rlt M (u n))) *)
intros n.
(* Goal: @eq bool (f n) false *)
now apply Bool.not_true_is_false.
Qed.

(** ** Corollaries *)

(* Goal: sumbool P (not P) *)
Lemma LPO_notforall : forall P : nat -> Prop, (forall n, P n \/ ~P n) ->
(* Goal: sumbool P (not P) *)
  (~ forall n : nat, ~ P n) -> exists n : nat, P n.
Proof.
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))) (_ : not (not (@ex nat (fun n : nat => P n)))), @ex nat (fun n : nat => P n) *)
  intros.
(* Goal: @ex nat (fun n : nat => P n) *)
  destruct (LPO P H).
(* Goal: @ex nat (fun n : nat => P n) *)
(* Goal: @ex nat (fun n : nat => P n) *)
  destruct s as (n,H1) ; exists n ; apply H1.
(* Goal: @ex nat (fun n : nat => P n) *)
  contradict H0 ; apply n.
Qed.

(* Goal: sumbool P (not P) *)
Lemma LPO_notnotexists : forall P : nat -> Prop, (forall n, P n \/ ~P n) ->
(* Goal: sumbool P (not P) *)
  ~~ (exists n : nat, P n) -> exists n : nat, P n.
Proof.
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))) (_ : not (not (@ex nat (fun n : nat => P n)))), @ex nat (fun n : nat => P n) *)
  intros.
(* Goal: @ex nat (fun n : nat => Rlt M (u n)) *)
  apply LPO_notforall.
(* Goal: Rle (IZR (Zpos xH)) x *)
  apply H.
(* Goal: not (forall n : nat, not (P n)) *)
  contradict H0.
(* Goal: not (@ex nat (fun n : nat => P n)) *)
  intros (n,H1).
(* Goal: False *)
  contradict H1 ; apply H0.
Qed.

(* Goal: sumbool P (not P) *)
Lemma LPO_ub_dec : forall (u : nat -> R),
  {M : R | forall n, u n <= M} + {forall M : R, exists n, M < u n}.
Proof.
(* Goal: forall u : forall _ : nat, R, sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  intros u.
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  destruct (LPO (fun M => forall n, u n <= (INR M))) as [ [M MHM] | HM ].
(* Goal: forall n : nat, or (forall n0 : nat, Rle (u n0) (INR n)) (not (forall n0 : nat, Rle (u n0) (INR n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  intros M.
(* Goal: or (forall n : nat, Rle (u n) (INR M)) (not (forall n : nat, Rle (u n) (INR M))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  destruct (LPO (fun n => INR M < u n)) as [[n Hn] | Hn].
(* Goal: forall n : nat, or (Rlt M (u n)) (not (Rlt M (u n))) *)
(* Goal: not (forall n : nat, not (Rlt M (u n))) *)
  intros n.
(* Goal: or (Rlt (INR M) (u n)) (not (Rlt (INR M) (u n))) *)
(* Goal: or (forall n : nat, Rle (u n) (INR M)) (not (forall n : nat, Rle (u n) (INR M))) *)
(* Goal: or (forall n : nat, Rle (u n) (INR M)) (not (forall n : nat, Rle (u n) (INR M))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  destruct (Rlt_dec (INR M) (u n)) as [H|H].
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
  now left.
(* Goal: E (IZR (Zpos xH)) *)
  now right.
(* Goal: or (forall n : nat, Rle (u n) (INR M)) (not (forall n : nat, Rle (u n) (INR M))) *)
(* Goal: or (forall n : nat, Rle (u n) (INR M)) (not (forall n : nat, Rle (u n) (INR M))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  right ; contradict Hn.
(* Goal: not (Rlt (INR M) (u n)) *)
(* Goal: or (forall n : nat, Rle (u n) (INR M)) (not (forall n : nat, Rle (u n) (INR M))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  now apply Rle_not_lt.
(* Goal: or (forall n : nat, Rle (u n) (INR M)) (not (forall n : nat, Rle (u n) (INR M))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  left ; intro n.
(* Goal: Rle (INR (S N)) (INR y) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  now apply Rnot_lt_le.
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  left ; now exists (INR M).
(* Goal: forall n : nat, or (forall n0 : nat, Rle (u n0) (INR n)) (not (forall n0 : nat, Rle (u n0) (INR n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
(* Goal: sumor (@sig R (fun M : R => forall n : nat, Rle (u n) M)) (forall M : R, @ex nat (fun n : nat => Rlt M (u n))) *)
  right ; intros M.
(* Goal: @ex nat (fun n : nat => Rlt M (u n)) *)
  destruct (nfloor_ex (Rbasic_fun.Rmax 0 M)) as [m Hm].
(* Goal: Rle (IZR Z0) (Rbasic_fun.Rmax (IZR Z0) M) *)
(* Goal: @ex nat (fun n : nat => Rlt M (u n)) *)
  now apply Rbasic_fun.Rmax_l.
(* Goal: @ex nat (fun n : nat => Rlt M (u n)) *)
  specialize (HM (S m)).
(* Goal: @ex nat (fun n : nat => Rlt M (u n)) *)
  apply LPO_notforall.
(* Goal: forall n : nat, or (Rlt M (u n)) (not (Rlt M (u n))) *)
(* Goal: not (forall n : nat, not (Rlt M (u n))) *)
  intros n.
(* Goal: or (Rlt M (u n)) (not (Rlt M (u n))) *)
(* Goal: not (forall n : nat, not (Rlt M (u n))) *)
  destruct (Rlt_dec M (u n)) as [H|H].
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
  now left.
(* Goal: E (IZR (Zpos xH)) *)
  now right.
(* Goal: forall n : nat, or (Rlt M (u n)) (not (Rlt M (u n))) *)
(* Goal: not (forall n : nat, not (Rlt M (u n))) *)
  contradict HM ; intros n.
(* Goal: Rle (u n) (INR (S m)) *)
  rewrite S_INR.
(* Goal: Rle (u n) (Rplus (INR m) (IZR (Zpos xH))) *)
  eapply Rle_trans, Rlt_le, Hm.
(* Goal: Rle (u n) (Rbasic_fun.Rmax (IZR Z0) M) *)
  eapply Rle_trans, Rbasic_fun.Rmax_r.
(* Goal: Rle (INR (S N)) (INR y) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  now apply Rnot_lt_le.
Qed.

(* Goal: sumbool P (not P) *)
(** * Excluded-middle and decidability *)

Lemma EM_dec :
  forall P : Prop, {not (not P)} + {not P}.
Proof.
(* Goal: forall P : Prop, sumbool (not (not P)) (not P) *)
intros P.
(* Goal: sumbool (not (not P)) (not P) *)
set (E := fun x => x = 0 \/ (x = 1 /\ P)).
(* Goal: sumbool (not (not P)) (not P) *)
destruct (completeness E) as [x H].
(* Goal: bound E *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumbool (not (not P)) (not P) *)
- exists 1.
(* Goal: sumbool P (not P) *)
  intros x [->|[-> _]].
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: Rle (IZR (Zpos xH)) (IZR (Zpos xH)) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumbool (not (not P)) (not P) *)
  apply Rle_0_1.
(* Goal: Rle (IZR Z0) (IZR Z0) *)
(* Goal: Rle y (IZR Z0) *)
(* Goal: sumbool (not (not P)) (not P) *)
  apply Rle_refl.
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumbool (not (not P)) (not P) *)
- exists 0.
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
  now left.
(* Goal: sumbool (not (not P)) (not P) *)
destruct (Rle_lt_dec 1 x) as [H'|H'].
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
- left.
(* Goal: not P *)
  intros HP.
(* Goal: False *)
(* Goal: sumbool (not (not P)) (not P) *)
  elim Rle_not_lt with (1 := H').
(* Goal: Rlt x (IZR (Zpos xH)) *)
(* Goal: sumbool (not (not P)) (not P) *)
  apply Rle_lt_trans with (2 := Rlt_0_1).
(* Goal: Rle (IZR (Zpos xH)) x *)
  apply H.
(* Goal: sumbool P (not P) *)
  intros y [->|[_ Hy]].
(* Goal: Rle (IZR Z0) (IZR Z0) *)
(* Goal: Rle y (IZR Z0) *)
(* Goal: sumbool (not (not P)) (not P) *)
  apply Rle_refl.
(* Goal: Rle y (IZR Z0) *)
(* Goal: sumbool (not (not P)) (not P) *)
  now elim HP.
(* Goal: E (IZR (Zpos xH)) *)
- right.
(* Goal: not P *)
  intros HP.
(* Goal: False *)
  apply Rlt_not_le with (1 := H').
(* Goal: Rle (IZR (Zpos xH)) x *)
  apply H.
(* Goal: E (IZR (Zpos xH)) *)
  right.
(* Goal: and (@eq R (IZR (Zpos xH)) (IZR (Zpos xH))) P *)
  now split.
Qed.

Lemma EM_dec' :
(* Goal: sumbool P (not P) *)
  forall P : Prop, P \/ not P -> {P} + {not P}.
Proof.
(* Goal: forall (P : Prop) (_ : or P (not P)), sumbool P (not P) *)
intros P HP.
(* Goal: sumbool P (not P) *)
destruct (EM_dec P) as [H|H].
(* Goal: sumbool P (not P) *)
(* Goal: sumbool P (not P) *)
- left.
(* Goal: P *)
(* Goal: sumbool P (not P) *)
  now destruct HP.
(* Goal: E (IZR (Zpos xH)) *)
- now right.
Qed.
