Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

This module proves some logical properties of the axiomatic of Reals.

Decidability of arithmetical statements.
Derivability of the Archimedean "axiom".
Decidability of negated formulas.

Require Import RIneq.

Decidability of arithmetical statements

One can iterate this lemma and use classical logic to decide any statement in the arithmetical hierarchy.

Section Arithmetical_dec.

Variable P : nat -> Prop.
Hypothesis HP : forall n, {P n} + {~P n}.

Lemma sig_forall_dec : {n | ~P n} + {forall n, P n}.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
{n : nat | ~ P n} + {forall n : nat, P n}
Proof.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
{n : nat | ~ P n} + {forall n : nat, P n}
assert (Hi: (forall n, 0 < INR n + 1)%R).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
forall n : nat, (0 < INR n + 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  intros n.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
n:nat
(0 < INR n + 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  apply Rle_lt_0_plus_1, pos_INR.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
set (u n := (if HP n then 0 else / (INR n + 1))%R).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
{n : nat | ~ P n} + {forall n : nat, P n}
assert (Bu: forall n, (u n <= 1)%R).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
forall n : nat, (u n <= 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  intros n.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
n:nat
(u n <= 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  unfold u.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
n:nat
((if HP n then 0 else / (INR n + 1)) <= 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  case HP ; intros _.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
n:nat
(0 <= 1)%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
n:nat
(/ (INR n + 1) <= 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  apply Rle_0_1.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
n:nat
(/ (INR n + 1) <= 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  rewrite <- S_INR, <- Rinv_1.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
n:nat
(/ INR (S n) <= / 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  apply Rinv_le_contravar with (1 := Rlt_0_1).P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
n:nat
(1 <= INR (S n))%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  apply (le_INR 1), le_n_S, le_0_n.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
{n : nat | ~ P n} + {forall n : nat, P n}
set (E y := exists n, y = u n).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
{n : nat | ~ P n} + {forall n : nat, P n}
destruct (completeness E) as [l [ub lub]].P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
bound E
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
exists x : R, E x
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  exists R1.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
is_upper_bound E R1
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
exists x : R, E x
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  intros y [n ->].P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
n:nat
(u n <= R1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
exists x : R, E x
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  apply Bu.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
exists x : R, E x
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  exists (u O).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
E (u 0)
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  now exists O.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
{n : nat | ~ P n} + {forall n : nat, P n}
assert (Hnp: forall n, not (P n) -> ((/ (INR n + 1) <= l)%R)).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  intros n Hp.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
n:nat
Hp:~ P n
(/ (INR n + 1) <= l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  apply ub.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
n:nat
Hp:~ P n
E (/ (INR n + 1))%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  exists n.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
n:nat
Hp:~ P n
(/ (INR n + 1))%R = u n
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  unfold u.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
n:nat
Hp:~ P n
(/ (INR n + 1))%R =
(if HP n then 0%R else (/ (INR n + 1))%R)
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  now destruct (HP n).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
destruct (Rle_lt_dec l 0) as [Hl|Hl].P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(l <= 0)%R
{n : nat | ~ P n} + {forall n : nat, P n}
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  right.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(l <= 0)%R
forall n : nat, P n
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  intros n.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
P n
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  destruct (HP n) as [H|H].P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
H:P n
P n
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
H:~ P n
P n
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  exact H.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
H:~ P n
P n
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  exfalso.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
H:~ P n
False
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  apply Rle_not_lt with (1 := Hl).P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
H:~ P n
(0 < l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  apply Rlt_le_trans with (/ (INR n + 1))%R.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
H:~ P n
(0 < / (INR n + 1))%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
H:~ P n
(/ (INR n + 1) <= l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  now apply Rinv_0_lt_compat.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(l <= 0)%R
n:nat
H:~ P n
(/ (INR n + 1) <= l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
  now apply Hnp.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n} + {forall n : nat, P n}
left.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
{n : nat | ~ P n}
set (N := Z.abs_nat (up (/l) - 2)).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
{n : nat | ~ P n}
assert (H1l: (1 <= /l)%R).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
(1 <= / l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
{n : nat | ~ P n}
  rewrite <- Rinv_1.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
(/ 1 <= / l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
{n : nat | ~ P n}
  apply Rinv_le_contravar with (1 := Hl).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
(l <= 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
{n : nat | ~ P n}
  apply lub.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
is_upper_bound E 1
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
{n : nat | ~ P n}
  now intros y [m ->].P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
{n : nat | ~ P n}
assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  unfold N.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(INR (Z.abs_nat (up (/ l) - 2)) + 1)%R =
(IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  rewrite INR_IZR_INZ.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (Z.of_nat (Z.abs_nat (up (/ l) - 2))) + 1)%R =
(IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  rewrite inj_Zabs_nat.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (Z.abs (up (/ l) - 2)) + 1)%R =
(IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (Z.abs (up (/ l) - 2)) + 1)%R =
(IZR (up (/ l) - 2) + 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l) - 2) + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  apply (f_equal (fun v => IZR v + 1)%R).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
Z.abs (up (/ l) - 2) = (up (/ l) - 2)%Z
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l) - 2) + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  apply Z.abs_eq.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(0 <= up (/ l) - 2)%Z
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l) - 2) + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  apply Zle_minus_le_0.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(2 <= up (/ l))%Z
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l) - 2) + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  apply (Zlt_le_succ 1).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(1 < up (/ l))%Z
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l) - 2) + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  apply lt_IZR.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(1 < IZR (up (/ l)))%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l) - 2) + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  apply Rle_lt_trans with (1 := H1l).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(/ l < IZR (up (/ l)))%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l) - 2) + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  apply archimed.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l) - 2) + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  rewrite minus_IZR.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l)) - 2 + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  simpl.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
(IZR (up (/ l)) - 2 + 1)%R = (IZR (up (/ l)) - 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
  ring.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
{n : nat | ~ P n}
assert (Hl': (/ (INR (S N) + 1) < l)%R).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
(/ (INR (S N) + 1) < l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
{n : nat | ~ P n}
  rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
(/ (INR (S N) + 1) < / / l)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
{n : nat | ~ P n}
  apply Rinv_1_lt_contravar with (1 := H1l).P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
(/ l < INR (S N) + 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
{n : nat | ~ P n}
  rewrite S_INR.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
(/ l < INR N + 1 + 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
{n : nat | ~ P n}
  rewrite HN.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
(/ l < IZR (up (/ l)) - 1 + 1)%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
{n : nat | ~ P n}
  ring_simplify.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
(/ l < IZR (up (/ l)))%R
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
{n : nat | ~ P n}
  apply archimed.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
{n : nat | ~ P n}
exists N.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
~ P N
intros H.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
False
apply Rle_not_lt with (2 := Hl').P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
(l <= / (INR (S N) + 1))%R
apply lub.P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
is_upper_bound E (/ (INR (S N) + 1))
intros y [n ->].P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
(u n <= / (INR (S N) + 1))%R
unfold u.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
((if HP n then 0 else / (INR n + 1)) <=
 / (INR (S N) + 1))%R
destruct (HP n) as [_|Hp].P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
(0 <= / (INR (S N) + 1))%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
(/ (INR n + 1) <= / (INR (S N) + 1))%R
  apply Rlt_le.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
(0 < / (INR (S N) + 1))%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
(/ (INR n + 1) <= / (INR (S N) + 1))%R
  now apply Rinv_0_lt_compat.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
(/ (INR n + 1) <= / (INR (S N) + 1))%R
apply Rinv_le_contravar.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
(0 < INR (S N) + 1)%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
(INR (S N) + 1 <= INR n + 1)%R
apply Hi.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
(INR (S N) + 1 <= INR n + 1)%R
apply Rplus_le_compat_r.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
(INR (S N) <= INR n)%R
apply le_INR.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
S N <= n
destruct (le_or_lt n N) as [Hn|Hn].P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
S N <= n
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:N < n
S N <= n
  2: now apply lt_le_S.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
S N <= n
exfalso.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
False
destruct (le_lt_or_eq _ _ Hn) as [Hn'| ->].P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
False
P:nat -> Prop
HP:forall n : nat, {P n} + {~ P n}
Hi:forall n : nat, (0 < INR n + 1)%R
u:=fun n : nat =>
if HP n then 0%R else (/ (INR n + 1))%R:nat -> R
Bu:forall n : nat, (u n <= 1)%R
E:=fun y : R => exists n : nat, y = u n:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n : nat, ~ P n -> (/ (INR n + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
Hn:N <= N
Hp:~ P N
False
2: now apply Hp.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
False
apply Rlt_not_le with (2 := Hnp _ Hp).P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(l < / (INR n + 1))%R
rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(/ / l < / (INR n + 1))%R
apply Rinv_1_lt_contravar.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(1 <= INR n + 1)%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(INR n + 1 < / l)%R
rewrite <- S_INR.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(1 <= INR (S n))%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(INR n + 1 < / l)%R
apply (le_INR 1), le_n_S, le_0_n.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(INR n + 1 < / l)%R
apply Rlt_le_trans with (INR N + 1)%R.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(INR n + 1 < INR N + 1)%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(INR N + 1 <= / l)%R
apply Rplus_lt_compat_r.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(INR n < INR N)%R
P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(INR N + 1 <= / l)%R
now apply lt_INR.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(INR N + 1 <= / l)%R
rewrite HN.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(IZR (up (/ l)) - 1 <= / l)%R
apply Rplus_le_reg_r with (-/l + 1)%R.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(IZR (up (/ l)) - 1 + (- / l + 1) <= / l + (- / l + 1))%R
ring_simplify.P:nat -> Prop
HP:forall n0 : nat, {P n0} + {~ P n0}
Hi:forall n0 : nat, (0 < INR n0 + 1)%R
u:=fun n0 : nat =>
if HP n0 then 0%R else (/ (INR n0 + 1))%R:nat -> R
Bu:forall n0 : nat, (u n0 <= 1)%R
E:=fun y : R => exists n0 : nat, y = u n0:R -> Prop
l:R
ub:is_upper_bound E l
lub:forall b : R, is_upper_bound E b -> (l <= b)%R
Hnp:forall n0 : nat, ~ P n0 -> (/ (INR n0 + 1) <= l)%R
Hl:(0 < l)%R
N:=Z.abs_nat (up (/ l) - 2):nat
H1l:(1 <= / l)%R
HN:(INR N + 1)%R = (IZR (up (/ l)) - 1)%R
Hl':(/ (INR (S N) + 1) < l)%R
H:P N
n:nat
Hp:~ P n
Hn:n <= N
Hn':n < N
(IZR (up (/ l)) - / l <= 1)%R
apply archimed.
Qed.

End Arithmetical_dec.

Derivability of the Archimedean axiom

This is a standard proof (it has been taken from PlanetMath). It is formulated negatively so as to avoid the need for classical logic. Using a proof of {n | ¬P n}+{∀ n, P n}, we can in principle also derive up and its specification. The proof above cannot be used for that purpose, since it relies on the archimed axiom.

Theorem not_not_archimedean :
  forall r : R, ~ (forall n : nat, (INR n <= r)%R).forall r : R, ~ (forall n : nat, (INR n <= r)%R)
Proof.forall r : R, ~ (forall n : nat, (INR n <= r)%R)
intros r H.r:R
H:forall n : nat, (INR n <= r)%R
False
set (E := fun r => exists n : nat, r = INR n).r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
False
assert (exists x : R, E x) by
  (exists 0%R; simpl; red; exists 0%nat; reflexivity).r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
False
assert (bound E) by (exists r; intros x (m,H2); rewrite H2; apply H).r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
False
destruct (completeness E) as (M,(H3,H4)); try assumption.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
False
set (M' := (M + -1)%R).r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
False
assert (H2 : ~ is_upper_bound E M').r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
~ is_upper_bound E M'
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
  intro H5.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
False
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
  assert (M <= M')%R by (apply H4; exact H5).r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
False
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
  apply (Rlt_not_le M M').r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M' < M)%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    unfold M'.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M + -1 < M)%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    pattern M at 2.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(fun r0 : R => (M + -1 < r0)%R) M
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    rewrite <- Rplus_0_l.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M + -1 < 0 + M)%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    pattern (0 + M)%R.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(fun r0 : R => (M + -1 < r0)%R) (0 + M)%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    rewrite Rplus_comm.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M + -1 < M + 0)%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    rewrite <- (Rplus_opp_r 1).r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M + -1 < M + (1 + - (1)))%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    apply Rplus_lt_compat_l.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(-1 < 1 + - (1))%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    rewrite Rplus_comm.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(-1 < - (1) + 1)%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
    apply Rlt_plus_1.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H5:is_upper_bound E M'
H2:(M <= M')%R
(M <= M')%R
r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
  assumption.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
False
apply H2.r:R
H:forall n : nat, (INR n <= r)%R
E:=fun r0 : R => exists n : nat, r0 = INR n:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
is_upper_bound E M'
intros N (n,H7).r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
(N <= M')%R
rewrite H7.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
(INR n <= M')%R
unfold M'.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
(INR n <= M + -1)%R
assert (H5 : (INR (S n) <= M)%R) by (apply H3; exists (S n); reflexivity).r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR (S n) <= M)%R
(INR n <= M + -1)%R
rewrite S_INR in H5.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
(INR n <= M + -1)%R
assert (H6 : (INR n + 1 + -1 <= M + -1)%R).r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
(INR n + 1 + -1 <= M + -1)%R
r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
H6:(INR n + 1 + -1 <= M + -1)%R
(INR n <= M + -1)%R
  apply Rplus_le_compat_r.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
(INR n + 1 <= M)%R
r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
H6:(INR n + 1 + -1 <= M + -1)%R
(INR n <= M + -1)%R
  assumption.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
H6:(INR n + 1 + -1 <= M + -1)%R
(INR n <= M + -1)%R
rewrite Rplus_assoc in H6.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
H6:(INR n + (1 + -1) <= M + -1)%R
(INR n <= M + -1)%R
rewrite Rplus_opp_r in H6.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
H6:(INR n + 0 <= M + -1)%R
(INR n <= M + -1)%R
rewrite (Rplus_comm (INR n) 0) in H6.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
H6:(0 + INR n <= M + -1)%R
(INR n <= M + -1)%R
rewrite Rplus_0_l in H6.r:R
H:forall n0 : nat, (INR n0 <= r)%R
E:=fun r0 : R => exists n0 : nat, r0 = INR n0:R -> Prop
H0:exists x : R, E x
H1:bound E
M:R
H3:is_upper_bound E M
H4:forall b : R, is_upper_bound E b -> (M <= b)%R
M':=(M + -1)%R:R
H2:~ is_upper_bound E M'
N:R
n:nat
H7:N = INR n
H5:(INR n + 1 <= M)%R
H6:(INR n <= M + -1)%R
(INR n <= M + -1)%R
assumption.
Qed.

Decidability of negated formulas

Lemma sig_not_dec : forall P : Prop, {not (not P)} + {not P}.forall P : Prop, {~ ~ P} + {~ P}
Proof.forall P : Prop, {~ ~ P} + {~ P}
intros P.P:Prop
{~ ~ P} + {~ P}
set (E := fun x => x = R0 \/ (x = R1 /\ P)).P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
{~ ~ P} + {~ P}
destruct (completeness E) as [x H].P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
bound E
P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
exists x : R, E x
P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
{~ ~ P} + {~ P}
  exists R1.P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
is_upper_bound E R1
P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
exists x : R, E x
P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
{~ ~ P} + {~ P}
  intros x [->|[-> _]].P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
(R0 <= R1)%R
P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
(R1 <= R1)%R
P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
exists x : R, E x
P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
{~ ~ P} + {~ P}
  apply Rle_0_1.P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
(R1 <= R1)%R
P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
exists x : R, E x
P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
{~ ~ P} + {~ P}
  apply Rle_refl.P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
exists x : R, E x
P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
{~ ~ P} + {~ P}
  exists R0.P:Prop
E:=fun x : R => x = R0 \/ x = R1 /\ P:R -> Prop
E R0
P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
{~ ~ P} + {~ P}
  now left.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
{~ ~ P} + {~ P}
destruct (Rle_lt_dec 1 x) as [H'|H'].P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
{~ ~ P} + {~ P}
P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(x < 1)%R
{~ ~ P} + {~ P}
-P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
{~ ~ P} + {~ P} left.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
~ ~ P
  intros HP.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
HP:~ P
False
  elim Rle_not_lt with (1 := H').P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
HP:~ P
(x < 1)%R
  apply Rle_lt_trans with (2 := Rlt_0_1).P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
HP:~ P
(x <= 0)%R
  apply H.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
HP:~ P
is_upper_bound E 0
  intros y [->|[_ Hy]].P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
HP:~ P
(R0 <= 0)%R
P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
HP:~ P
y:R
Hy:P
(y <= 0)%R
  apply Rle_refl.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(1 <= x)%R
HP:~ P
y:R
Hy:P
(y <= 0)%R
  now elim HP.
-P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(x < 1)%R
{~ ~ P} + {~ P} right.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(x < 1)%R
~ P
  intros HP.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(x < 1)%R
HP:P
False
  apply Rlt_not_le with (1 := H').P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(x < 1)%R
HP:P
(1 <= x)%R
  apply H.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(x < 1)%R
HP:P
E 1%R
  right.P:Prop
E:=fun x0 : R => x0 = R0 \/ x0 = R1 /\ P:R -> Prop
x:R
H:is_lub E x
H':(x < 1)%R
HP:P
1%R = R1 /\ P
  now split.
Qed.