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

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

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

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

Require Import Reals.
Require Import mathcomp.ssreflect.ssreflect.
Require Import List.

(** This file describes compactness results: finite covering of opens,
finite covering based on a gauge function, specific instances for 1D
and 2D spaces. *)

(* This enables a compatibility with Coq 8.4, which didn't have the right lemmas Rplus_lt_reg_l
   and Rplus_lt_reg_r.  So this Import should disappear in the future.  A better solution would
   be to have the fix in a specific compatibility file, rather than in Rcomplements.v. *)
Require Import Rcomplements.

Open Scope R_scope.

Lemma completeness_any :
  forall P : R -> Prop,
  ( forall x y, x <= y -> P y -> P x ) ->
  forall He : (exists x, P x),
  forall Hb : (bound P),
  forall x, x < proj1_sig (completeness _ Hb He) ->
  ~ ~ P x.
Proof.
(* Goal: forall (P : forall _ : R, Prop) (_ : forall (x y : R) (_ : Rle x y) (_ : P y), P x) (He : @ex R (fun x : R => P x)) (Hb : bound P) (x : R) (_ : Rlt x (@proj1_sig R (fun m : R => is_lub P m) (completeness P Hb He))), not (not (P x)) *)
intros P HP He Hb x.
(* Goal: forall (_ : P (Rmin b (Rplus (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) (pos d)))) (_ : Rlt (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) b), False *)
case completeness => y [Hy1 Hy2] /= Hxy Px.
(* Goal: False *)
apply Rle_not_lt with (2 := Hxy).
(* Goal: forall (_ : P (Rmin b (Rplus (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) (pos d)))) (_ : Rlt (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) b), False *)
apply Hy2 => t Pt.
(* Goal: forall (_ : P (Rmin b (Rplus (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) (pos d)))) (_ : Rlt (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) b), False *)
apply Rnot_lt_le => Hxt.
(* Goal: False *)
apply Px.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply: HP Pt.
(* Goal: Rle x t *)
now apply Rlt_le.
Qed.

Lemma false_not_not :
  forall P Q : Prop, (P -> ~Q) -> (~~P -> ~Q).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, not Q) (_ : not (not P)), not Q *)
intros P Q H HP HQ.
(* Goal: False *)
apply HP.
(* Goal: not P *)
intros H'.
(* Goal: False *)
now apply H.
Qed.

Section Compactness.

Fixpoint Tn n T : Type :=
  match n with
  | O => unit
  | S n => (T * Tn n T)%type
  end.

Fixpoint bounded_n n : Tn n R -> Tn n R -> Tn n R -> Prop :=
  match n return Tn n R -> Tn n R -> Tn n R -> Prop with
  | O => fun a b x : Tn O R => True
  | S n => fun a b x : Tn (S n) R =>
    let '(a1,a2) := a in
    let '(b1,b2) := b in
    let '(x1,x2) := x in
    a1 <= x1 <= b1 /\ bounded_n n a2 b2 x2
  end.

Fixpoint close_n n d : Tn n R -> Tn n R -> Prop :=
  match n return Tn n R -> Tn n R -> Prop with
  | O => fun x t : Tn O R => True
  | S n => fun x t : Tn (S n) R =>
    let '(x1,x2) := x in
    let '(t1,t2) := t in
    Rabs (x1 - t1) < d /\ close_n n d x2 t2
  end.

(** * Compactness: there is a finite covering of opens *)

Lemma compactness_list :
  forall n a b (delta : Tn n R -> posreal),
  ~~ exists l, forall x, bounded_n n a b x -> exists t, In t l /\ bounded_n n a b t /\ close_n n (delta t) x t.
Proof.
(* Goal: close_n n (pos (delta x)) x x *)
(* Goal: Rle (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
induction n.
(* Goal: forall (a b : R) (delta : forall _ : R, posreal), @sig posreal (fun d : posreal => forall (x : R) (_ : and (Rle a x) (Rle x b)), not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t)))))))) *)
intros a b delta.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros H.
(* Goal: False *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply H.
(* Goal: @ex (list (Tn O R)) (fun l : list (Tn O R) => forall (x : Tn O R) (_ : bounded_n O a b x), @ex (Tn O R) (fun t : Tn O R => and (@In (Tn O R) t l) (and (bounded_n O a b t) (close_n O (pos (delta t)) x t)))) *)
(* Goal: forall (a b : Tn (S n) R) (delta : forall _ : Tn (S n) R, posreal), not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) a b x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) a b t) (close_n (S n) (pos (delta t)) x t)))))) *)
exists (tt :: nil).
(* Goal: forall (x : R) (_ : and (Rle a x) (Rle x b)), not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))))) *)
intros x Hx.
(* Goal: @ex (Tn O R) (fun t : Tn O R => and (@In (Tn O R) t (@Datatypes.cons unit tt (@Datatypes.nil unit))) (and (bounded_n O a b t) (close_n O (pos (delta t)) x t))) *)
(* Goal: forall (a b : Tn (S n) R) (delta : forall _ : Tn (S n) R, posreal), not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) a b x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) a b t) (close_n (S n) (pos (delta t)) x t)))))) *)
exists tt.
(* Goal: and (and (and (Rle a a) (Rle a b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus a a)) (pos (delta (@pair R (Tn n R) a t')))) (close_n n (pos (delta (@pair R (Tn n R) a t'))) x' t')) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
repeat split.
(* Goal: @In (Tn O R) tt (@Datatypes.cons unit tt (@Datatypes.nil unit)) *)
(* Goal: forall (a b : Tn (S n) R) (delta : forall _ : Tn (S n) R, posreal), not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) a b x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) a b t) (close_n (S n) (pos (delta t)) x t)))))) *)
now left.
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* *)
(* Goal: forall (a b : prod R (Tn n R)) (delta : forall _ : prod R (Tn n R), posreal), not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair a1 a2 := a in let 'pair b1 b2 := b in let 'pair x1 x2 := x in and (and (Rle a1 x1) (Rle x1 b1)) (bounded_n n a2 b2 x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair a1 a2 := a in let 'pair b1 b2 := b in let 'pair x1 x2 := t in and (and (Rle a1 x1) (Rle x1 b1)) (bounded_n n a2 b2 x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros (a,a') (b,b') delta.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct (Rlt_le_dec b a) as [Hab|Hab].
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros H.
(* Goal: False *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply H.
(* Goal: @ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
exists nil.
(* Goal: forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@Datatypes.nil (prod R (Tn n R)))) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros (x,x') (Hx,_).
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@Datatypes.nil (prod R (Tn n R)))) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
elim (Rlt_irrefl a).
(* Goal: Rlt a a *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Rle_lt_trans with (2 := Hab).
(* Goal: Rle a b *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now apply Rle_trans with x.
(* *)
set (P y := y <= b /\ ~~exists l, forall x, bounded_n (S n) (a,a') (y,b') x ->
  exists t, In t l /\ bounded_n (S n) (a,a') (b,b') t /\ close_n (S n) (delta t) x t).
(* . *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
assert (P1': P a).
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle a b *)
(* Goal: not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) a b') x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x t)))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Hab.
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 a)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
specialize (IHn a' b' (fun x' => delta (a,x'))).
(* Goal: not (@ex (list (Tn n R)) (fun l : list (Tn n R) => forall (x : Tn n R) (_ : bounded_n n a' b' x), @ex (Tn n R) (fun t : Tn n R => and (@In (Tn n R) t l) (and (bounded_n n a' b' t) (close_n n (pos (delta (@pair R (Tn n R) y t))) x t))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
contradict IHn.
(* Goal: not (@ex (list (Tn n R)) (fun l : list (Tn n R) => forall (x : Tn n R) (_ : bounded_n n a' b' x), @ex (Tn n R) (fun t : Tn n R => and (@In (Tn n R) t l) (and (bounded_n n a' b' t) (close_n n (pos (delta (@pair R (Tn n R) y t))) x t))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
contradict IHn.
(* Goal: @ex posreal (fun d : posreal => P (Rmin b (Rplus y (pos d)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct IHn as (l,Hl).
(* Goal: @ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 a)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
exists (fold_right (fun x' acc => (a,x')::acc) nil l).
(* Goal: forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 (Rmin b (Rplus y (Rdiv (pos d) (IZR (Zpos (xO xH)))))))) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros (x,x') (Hx,Hx').
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) a x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
replace x with a by now apply Rle_antisym.
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct (Hl x' Hx') as (t',(Ht1,Ht2)).
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) a x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus a t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
exists (a,t').
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
clear -Ht1.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
induction l.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
easy.
(* Goal: @In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) (@Datatypes.cons (Tn n R) a0 l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
simpl in Ht1 |- *.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
destruct Ht1 as [Ht1|Ht1].
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
left.
(* Goal: @eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t') *)
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now apply f_equal2.
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
right.
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l)) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
now apply IHl.
(* Goal: and (and (and (Rle a a) (Rle a b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus a a)) (pos (delta (@pair R (Tn n R) a t')))) (close_n n (pos (delta (@pair R (Tn n R) a t'))) x' t')) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
repeat split.
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) (@Datatypes.nil (Tn n R)))) (IZR (Zpos xH)) *)
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) (@Datatypes.cons (Tn n R) a l))) (IZR (Zpos xH)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos v) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rle_refl.
(* Goal: Rle a b *)
(* Goal: bounded_n n a' b' t' *)
(* Goal: Rlt (Rabs (Rminus a a)) (pos (delta (@pair R (Tn n R) a t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) a t'))) x' t' *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
exact Hab.
(* Goal: close_n n (pos (delta t)) x t *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Ht2.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite /Rminus Rplus_opp_r Rabs_R0.
(* Goal: Rlt (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply cond_pos.
(* Goal: close_n n (pos (delta t)) x t *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Ht2.
(* . *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
assert (P2: bound P).
(* Goal: forall (_ : P (Rmin b (Rplus (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) (pos d)))) (_ : Rlt (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) b), False *)
exists b => y Hy.
(* Goal: Rle y b *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Hy.
(* . *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
assert (P3: forall x y, x <= y -> P y -> P x).
(* Goal: forall (x y : R) (_ : Rle x y) (_ : P y), P x *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros x y Hxy (Py1,Py2).
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle x b *)
(* Goal: not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x0 : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) x b') x0), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x0 t)))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now apply Rle_trans with y.
(* Goal: not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) y b') x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x t))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
contradict Py2.
(* Goal: not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) y b') x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x t))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
contradict Py2.
(* Goal: @ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x0 : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) x b') x0), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x0 t)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct Py2 as (l,Py2).
(* Goal: forall (_ : P (Rmin b (Rplus (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) (pos d)))) (_ : Rlt (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) b), False *)
exists l => [[z z']] Hz.
(* Goal: @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) (@pair R ((fix Tn (n : nat) (T : Type) {struct n} : Type := match n with | O => unit | S n0 => prod T (Tn n0 T) end) n R) z z') t))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Py2.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: bounded_n n a' b' z' *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Hz.
(* Goal: Rle z y *)
(* Goal: bounded_n n a' b' z' *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now apply Rle_trans with (1 := proj2 (proj1 Hz)).
(* Goal: bounded_n n a' b' z' *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Hz.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
assert (P1: exists x, P x).
(* Goal: @ex R (fun x : R => P x) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now exists a.
(* . *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
set (y := proj1_sig (completeness _ P2 P1)).
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
assert (P4: ~~exists d : posreal, P (Rmin b (y + d))).
(* Goal: not (not (@ex posreal (fun d : posreal => P (Rmin b (Rplus y (pos d)))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
specialize (IHn a' b' (fun x' => delta (y,x'))).
(* Goal: not (@ex (list (Tn n R)) (fun l : list (Tn n R) => forall (x : Tn n R) (_ : bounded_n n a' b' x), @ex (Tn n R) (fun t : Tn n R => and (@In (Tn n R) t l) (and (bounded_n n a' b' t) (close_n n (pos (delta (@pair R (Tn n R) y t))) x t))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
contradict IHn.
(* Goal: not (@ex (list (Tn n R)) (fun l : list (Tn n R) => forall (x : Tn n R) (_ : bounded_n n a' b' x), @ex (Tn n R) (fun t : Tn n R => and (@In (Tn n R) t l) (and (bounded_n n a' b' t) (close_n n (pos (delta (@pair R (Tn n R) y t))) x t))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
contradict IHn.
(* Goal: @ex posreal (fun d : posreal => P (Rmin b (Rplus y (pos d)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct IHn as (l, Hl).
(* Goal: @ex posreal (fun d : posreal => P (Rmin b (Rplus y (pos d)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
set (d := fold_right (fun t acc => mkposreal _ (Rmin_stable_in_posreal (delta (y,t)) acc)) (mkposreal _ Rlt_0_1) l).
(* Goal: @ex posreal (fun d : posreal => P (Rmin b (Rplus y (pos d)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
assert (Hd: 0 < d/2).
(* Goal: Rlt (IZR Z0) (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) *)
apply Fourier_util.Rlt_mult_inv_pos.
(* Goal: Rlt (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply cond_pos.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
apply Rlt_R0_R2.
(* Goal: @ex posreal (fun d : posreal => P (Rmin b (Rplus y (pos d)))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
exists (mkposreal _ Hd).
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle (Rmin (pos (delta t)) (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l))) (pos (delta t)) *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rmin_l.
(* Goal: not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) (Rmin b (Rplus y (pos (mkposreal (Rdiv (pos d) (IZR (Zpos (xO xH)))) Hd)))) b') x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x t)))))) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
refine (_ (completeness_any _ P3 P1 P2 (y - d) _)).
(* Goal: forall _ : not (not (P (Rminus y (pos d)))), not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x0 : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) (Rmin b (Rplus y (pos (mkposreal (Rdiv (pos d) (IZR (Zpos (xO xH)))) Hd)))) b') x0), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x0 t)))))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros Hy.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply: false_not_not Hy => Hy.
(* Goal: not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) (Rmin b (Rplus y (pos (mkposreal (Rdiv (pos d) (IZR (Zpos (xO xH)))) Hd)))) b') x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x t)))))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct Hy as (Hy1,Hy2).
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply: false_not_not Hy2 => Hy2.
(* Goal: not (not (@ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) (Rmin b (Rplus y (pos (mkposreal (Rdiv (pos d) (IZR (Zpos (xO xH)))) Hd)))) b') x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x t)))))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply.
(* Goal: @ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) (Rmin b (Rplus y (pos (mkposreal (Rdiv (pos d) (IZR (Zpos (xO xH)))) Hd)))) b') x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x t)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct Hy2 as (l',Hl').
(* Goal: @ex (list (Tn (S n) R)) (fun l : list (Tn (S n) R) => forall (x : Tn (S n) R) (_ : bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) (Rmin b (Rplus y (pos (mkposreal (Rdiv (pos d) (IZR (Zpos (xO xH)))) Hd)))) b') x), @ex (Tn (S n) R) (fun t : Tn (S n) R => and (@In (Tn (S n) R) t l) (and (bounded_n (S n) (@pair R (Tn n R) a a') (@pair R (Tn n R) b b') t) (close_n (S n) (pos (delta t)) x t)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
exists (app (fold_right (fun x' acc => (y,x')::acc) nil l) l').
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* Goal: forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 (Rmin b (Rplus y (Rdiv (pos d) (IZR (Zpos (xO xH)))))))) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros (x,x') (Hx,Hx').
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct (Rle_or_lt x (y - d)) as [Hxy|Hxy].
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct (Hl' (x,x') (conj (conj (proj1 Hx) Hxy) Hx')) as (t,(Ht1,Ht2)).
(* Goal: @ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))) *)
exists t.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: @In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l') *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply in_or_app.
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now right.
(* Goal: and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)) *)
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
exact Ht2.
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct (Hl x' Hx') as (t',(Ht1,Ht2)).
(* Goal: @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l')) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x t1)) (pos (delta t))) (close_n n (pos (delta t)) x' t2)))) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
exists (y, t').
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: @In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@app (prod R (Tn n R)) (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l) l') *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply in_or_app.
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
left.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
clear -Ht1.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
induction l.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
easy.
(* Goal: @In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) (@Datatypes.cons (Tn n R) a0 l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
simpl in Ht1 |- *.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
destruct Ht1 as [Ht1|Ht1].
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
left.
(* Goal: @eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t') *)
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now apply f_equal2.
(* Goal: or (@eq (prod R (Tn n R)) (@pair R (Tn n R) y a0) (@pair R (Tn n R) y t')) (@In (prod R (Tn n R)) (@pair R (Tn n R) y t') (@fold_right (list (prod R (Tn n R))) (Tn n R) (fun (x' : Tn n R) (acc : list (prod R (Tn n R))) => @Datatypes.cons (prod R (Tn n R)) (@pair R (Tn n R) y x') acc) (@Datatypes.nil (prod R (Tn n R))) l)) *)
(* Goal: and (and (and (Rle a y) (Rle y b)) (bounded_n n a' b' t')) (and (Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t')))) (close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t')) *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
right.
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l)) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
now apply IHl.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
do 2 split.
(* Goal: and (Rle a y) (Rle y b) *)
(* Goal: bounded_n n a' b' t' *)
(* Goal: Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
unfold y.
(* Goal: forall (_ : P (Rmin b (Rplus (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) (pos d)))) (_ : Rlt (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) b), False *)
case completeness => /= z [Hz1 Hz2].
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle a z *)
(* Goal: Rle z b *)
(* Goal: bounded_n n a' b' t' *)
(* Goal: Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now apply Hz1.
(* Goal: Rle z b *)
(* Goal: bounded_n n a' b' t' *)
(* Goal: Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Hz2.
(* Goal: is_upper_bound P b *)
(* Goal: bounded_n n a' b' t' *)
(* Goal: Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
intros w Hw.
(* Goal: Rle w b *)
(* Goal: bounded_n n a' b' t' *)
(* Goal: Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Hw.
(* Goal: close_n n (pos (delta t)) x t *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Ht2.
(* Goal: Rlt (Rabs (Rminus x y)) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Rlt_le_trans with d.
(* Goal: Rlt (Rabs (Rminus x y)) (pos d) *)
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Rabs_def1.
(* Goal: Rlt (Rminus x y) (pos d) *)
(* Goal: Rlt (Ropp (pos d)) (Rminus x y) *)
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Rplus_lt_reg_r with y.
(* Goal: Rlt (Rplus (Rminus x y) y) (Rplus (pos d) y) *)
(* Goal: Rlt (Ropp (pos d)) (Rminus x y) *)
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
ring_simplify.
(* Goal: Rlt x (Rplus y (pos d)) *)
(* Goal: Rlt (Ropp (pos d)) (Rminus x y) *)
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Rle_lt_trans with (y + d/2).
(* Goal: Rle x (Rplus y (Rdiv (pos d) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rplus y (Rdiv (pos d) (IZR (Zpos (xO xH))))) (Rplus y (pos d)) *)
(* Goal: Rlt (Ropp (pos d)) (Rminus x y) *)
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now apply Rle_trans with (2 := Rmin_r b _).
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))))) *)
apply Rplus_lt_compat_l.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite -(Rplus_0_r (d/2)).
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite {2}(double_var d).
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))))) *)
now apply Rplus_lt_compat_l.
(* Goal: Rlt (Ropp (pos d)) (Rminus x y) *)
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Rplus_lt_reg_l with y.
(* Goal: Rlt (Rplus y (Ropp (pos d))) (Rplus y (Rminus x y)) *)
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
now ring_simplify (y + (x - y)).
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
clearbody y.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
clear -Ht1.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
induction l.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
easy.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
simpl in Ht1.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
destruct Ht1 as [Ht1|Ht1].
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite -Ht1.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply: Rmin_l.
(* Goal: Rle (pos d) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
unfold d.
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* Goal: Rle (Rmin (pos (delta (@pair R (Tn n R) y a))) (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta (@pair R (Tn n R) y t))) (pos acc)) (Rmin_stable_in_posreal (delta (@pair R (Tn n R) y t)) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l))) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Rle_trans with (1 := Rmin_r _ _).
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l)) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
now apply IHl.
(* Goal: close_n n (pos (delta t)) x t *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Ht2.
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
fold y.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite -{2}(Rplus_0_r y) -Ropp_0.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))))) *)
apply Rplus_lt_compat_l.
(* Goal: Rlt (Ropp (pos d)) (Ropp (IZR Z0)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Ropp_lt_contravar.
(* Goal: Rlt (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply cond_pos.
(* . *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply: false_not_not P4 => P4.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct P4 as (d,P4).
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
destruct (Rle_or_lt b y) as [Hby|Hby].
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite Rmin_left in P4.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
(* Goal: Rle b (Rplus y (pos d)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply P4.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite -(Rplus_0_r b).
(* Goal: Rle (Rplus b (IZR Z0)) (Rplus y (pos d)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
apply Rplus_le_compat with (1 := Hby).
(* Goal: Rle (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rlt_le.
(* Goal: Rlt (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply cond_pos.
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
elimtype False.
(* Goal: False *)
unfold y in *.
(* Goal: False *)
clear y.
(* Goal: False *)
revert P4 Hby.
(* Goal: forall (_ : P (Rmin b (Rplus (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) (pos d)))) (_ : Rlt (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) b), False *)
case completeness => /= y [Hy1 Hy2] P4 Hby.
(* Goal: False *)
apply Rle_not_lt with (1 := Hy1 (Rmin b (y + d)) P4).
(* Goal: Rlt y (Rmin b (Rplus y (pos d))) *)
apply Rmin_case.
(* Goal: Rlt y b *)
(* Goal: Rlt y (Rplus y (pos d)) *)
exact Hby.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite -{1}(Rplus_0_r y).
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))))) *)
apply Rplus_lt_compat_l.
(* Goal: Rlt (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply cond_pos.
Qed.

(** * Compactness: there is a covering based on a gauge function *)

Lemma compactness_value :
  forall n a b (delta : Tn n R -> posreal),
  { d : posreal | forall x, bounded_n n a b x -> ~~ exists t, bounded_n n a b t /\ close_n n (delta t) x t /\ d <= delta t }.
Proof.
(* Goal: forall (n : nat) (a b : Tn n R) (delta : forall _ : Tn n R, posreal), @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
intros n a b delta.
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
set (P d := d <= 1 /\ forall x, bounded_n n a b x -> exists t, bounded_n n a b t /\ close_n n (delta t) x t /\ d <= delta t).
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
assert (P1 : exists d, P d).
(* Goal: @ex R (fun d : R => P d) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
exists 0.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (IZR Z0) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rle_0_1.
(* Goal: forall (x : R) (_ : and (Rle a x) (Rle x b)), not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))))) *)
intros x Hx.
(* Goal: @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (IZR Z0) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
exists x.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: bounded_n n a b x *)
(* Goal: and (close_n n (pos (delta x)) x x) (Rle (IZR Z0) (pos (delta x))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
exact Hx.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l)) (IZR (Zpos xH)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos v) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
clear.
(* Goal: close_n n (pos (delta x)) x x *)
(* Goal: Rle (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
induction n.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
easy.
(* Goal: close_n (S n) (pos (delta x)) x x *)
(* Goal: Rle (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
destruct x as (x,x').
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite /Rminus Rplus_opp_r Rabs_R0.
(* Goal: Rlt (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply cond_pos.
(* Goal: close_n n (pos (delta (@pair R (Tn n R) x x'))) x' x' *)
(* Goal: Rle (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply (IHn (fun x' => delta (x,x'))).
(* Goal: Rle (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rlt_le.
(* Goal: Rlt (IZR Z0) (pos (delta x)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply cond_pos.
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
assert (P2 : bound P).
(* Goal: bound P *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
exists 1.
(* Goal: is_upper_bound P (IZR (Zpos xH)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
now intros d (Hd,_).
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
set (d := completeness P P2 P1).
(* *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
assert (P3 : 0 < proj1_sig d).
(* Goal: Rlt (IZR Z0) (@proj1_sig R (fun m : R => is_lub P m) d) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
revert d.
(* Goal: let d := completeness P P2 P1 in Rlt (IZR Z0) (@proj1_sig R (fun m : R => is_lub P m) d) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
case completeness.
(* Goal: forall (x : R) (i : is_lub P x), let d := @exist R (fun m : R => is_lub P m) x i in Rlt (IZR Z0) (@proj1_sig R (fun m : R => is_lub P m) d) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
intros d (Hd1,Hd2).
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* Goal: Rlt (IZR Z0) d *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rnot_le_lt.
(* Goal: not (Rle d (IZR Z0)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
intros Hd3.
(* Goal: False *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply (compactness_list n a b delta).
(* Goal: not (@ex (list (Tn n R)) (fun l : list (Tn n R) => forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (@In (Tn n R) t l) (and (bounded_n n a b t) (close_n n (pos (delta t)) x t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
intros (l,Hl).
(* Goal: False *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
set (v := fold_right (fun t acc => mkposreal _ (Rmin_stable_in_posreal (delta t) acc)) (mkposreal _ Rlt_0_1) l).
(* Goal: False *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply (Rlt_not_le _ _ (cond_pos v)).
(* Goal: Rle (pos v) (IZR Z0) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rle_trans with (2 := Hd3).
(* Goal: Rle (pos v) d *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Hd1.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle (pos v) (IZR (Zpos xH)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos v) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
unfold v.
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l)) (IZR (Zpos xH)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos v) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
clear.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
induction l.
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) (@Datatypes.nil (Tn n R)))) (IZR (Zpos xH)) *)
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) (@Datatypes.cons (Tn n R) a l))) (IZR (Zpos xH)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos v) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rle_refl.
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* Goal: Rle (Rmin (pos (delta a)) (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l))) (IZR (Zpos xH)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos v) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rle_trans with (2 := IHl).
(* Goal: Rle (Rmin (pos (delta a)) (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l))) (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos v) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rmin_r.
(* Goal: forall (x : R) (_ : and (Rle a x) (Rle x b)), not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))))) *)
intros x Hx.
(* Goal: @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos v) (pos (delta t))))) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
destruct (Hl x Hx) as (t,(Ht1,Ht2)).
(* Goal: @ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))) *)
exists t.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: close_n n (pos (delta t)) x t *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Ht2.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: close_n n (pos (delta t)) x t *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Ht2.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
clear -Ht1.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
induction l.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
easy.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
simpl in Ht1.
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
destruct Ht1 as [Ht1|Ht1].
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite Ht1.
(* Goal: Rle (Rmin (pos (delta t)) (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l))) (pos (delta t)) *)
(* Goal: Rle (pos v) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
apply Rmin_l.
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* Goal: Rle (Rmin (pos (delta (@pair R (Tn n R) y a))) (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta (@pair R (Tn n R) y t))) (pos acc)) (Rmin_stable_in_posreal (delta (@pair R (Tn n R) y t)) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l))) (pos (delta (@pair R (Tn n R) y t'))) *)
(* Goal: close_n n (pos (delta (@pair R (Tn n R) y t'))) x' t' *)
(* Goal: Rlt (Rminus y (pos d)) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
(* Goal: not (not (@ex (list (prod R (Tn n R))) (fun l : list (prod R (Tn n R)) => forall (x : prod R (Tn n R)) (_ : let 'pair x1 x2 := x in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)), @ex (prod R (Tn n R)) (fun t : prod R (Tn n R) => and (@In (prod R (Tn n R)) t l) (and (let 'pair x1 x2 := t in and (and (Rle a x1) (Rle x1 b)) (bounded_n n a' b' x2)) (let 'pair x1 x2 := x in let 'pair t1 t2 := t in and (Rlt (Rabs (Rminus x1 t1)) (pos (delta t))) (close_n n (pos (delta t)) x2 t2))))))) *)
eapply Rle_trans with (1 := Rmin_r _ _).
(* Goal: Rle (pos (@fold_right posreal (Tn n R) (fun (t : Tn n R) (acc : posreal) => mkposreal (Rmin (pos (delta t)) (pos acc)) (Rmin_stable_in_posreal (delta t) acc)) (mkposreal (IZR (Zpos xH)) Rlt_0_1) l)) (pos (delta t)) *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
now apply IHl.
(* *)
(* Goal: @sig posreal (fun d : posreal => forall (x : Tn n R) (_ : bounded_n n a b x), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos d) (pos (delta t)))))))) *)
exists (mkposreal _ (Fourier_util.Rlt_mult_inv_pos _ _ P3 Rlt_R0_R2)).
(* Goal: forall (x : R) (_ : and (Rle a x) (Rle x b)), not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))))) *)
intros x Hx.
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (pos (mkposreal (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (Fourier_util.Rlt_mult_inv_pos (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))) P3 Rlt_R0_R2))) (pos (delta t))))))) *)
simpl.
(* Goal: not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (pos (delta t))))))) *)
refine (_ (completeness_any P _ P1 P2 (proj1_sig d / 2) _)).
(* Goal: forall _ : not (not (P (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))))), not (not (@ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (pos (delta t))))))) *)
(* Goal: forall (x y : R) (_ : Rle x y) (_ : P y), P x *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
intros HP.
(* Goal: not (P (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))))) *)
(* Goal: forall (x y : R) (_ : Rle x y) (_ : P y), P x *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
contradict HP.
(* Goal: not (P (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))))) *)
(* Goal: forall (x y : R) (_ : Rle x y) (_ : P y), P x *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
contradict HP.
(* Goal: @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle (Rmult (@proj1_sig R (fun m : R => is_lub P m) d) (Rinv (IZR (Zpos (xO xH))))) (pos (delta t))))) *)
(* Goal: forall (x y : R) (_ : Rle x y) (_ : P y), P x *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
destruct HP as (_,HP).
(* Goal: False *)
now apply HP.
(* Goal: forall (x y : R) (_ : Rle x y) (_ : P y), P x *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
intros u v Huv (Pv1,Pv2).
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle u (IZR (Zpos xH)) *)
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle u (pos (delta t))))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
now apply Rle_trans with v.
(* Goal: forall (x : Tn n R) (_ : bounded_n n a b x), @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) x t) (Rle u (pos (delta t))))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
intros z Hz.
(* Goal: @ex (Tn n R) (fun t : Tn n R => and (bounded_n n a b t) (and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
destruct (Pv2 z Hz) as (t,Ht).
(* Goal: @ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))) *)
exists t.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle v (pos (delta t)) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
apply Ht.
(* Goal: and (close_n n (pos (delta t)) z t) (Rle u (pos (delta t))) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
split.
(* Goal: Rle v (pos (delta t)) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
apply Ht.
(* Goal: Rle u (pos (delta t)) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
apply Rle_trans with (1 := Huv).
(* Goal: Rle v (pos (delta t)) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
apply Ht.
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
fold d.
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite -(Rplus_0_r (proj1_sig d / 2)).
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (@proj1_sig R (fun m : R => is_lub P m) d) *)
rewrite {2}(double_var (proj1_sig d)).
(* Goal: Rlt (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (IZR Z0)) (Rplus (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH))))) *)
apply Rplus_lt_compat_l.
(* Goal: Rlt (IZR Z0) (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) *)
apply Fourier_util.Rlt_mult_inv_pos.
(* Goal: Rlt (IZR Z0) (@proj1_sig R (fun m : R => is_lub P m) d) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
exact P3.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
apply Rlt_R0_R2.
Qed.

End Compactness.

(** * Specific instances of compactness for 1D and 2D spaces *)

Lemma compactness_value_1d :
  forall a b (delta : R -> posreal),
  { d : posreal | forall x, a <= x <= b -> ~~ exists t, a <= t <= b /\ Rabs (x - t) < delta t /\ d <= delta t }.
Proof.
(* Goal: forall (a b : R) (delta : forall _ : R, posreal), @sig posreal (fun d : posreal => forall (x : R) (_ : and (Rle a x) (Rle x b)), not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t)))))))) *)
intros a b delta.
(* Goal: @sig posreal (fun d : posreal => forall (x : R) (_ : and (Rle a x) (Rle x b)), not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t)))))))) *)
destruct (compactness_value 1 (a,tt) (b,tt) (fun t => let '(t,_) := t in delta t)) as (d, Hd).
(* Goal: @sig posreal (fun d : posreal => forall (x y : R) (_ : and (Rle a x) (Rle x b)) (_ : and (Rle a' y) (Rle y b')), not (not (@ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v))))))))))) *)
exists d.
(* Goal: forall (x : R) (_ : and (Rle a x) (Rle x b)), not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))))) *)
intros x Hx.
(* Goal: not (not (@ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))))) *)
specialize (Hd (x,tt) (conj Hx I)).
(* Goal: not (not (@ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v)))))))))) *)
do 2 contradict Hd.
(* Goal: @ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))) *)
destruct Hd as ((t,t'),Ht).
(* Goal: @ex R (fun t : R => and (and (Rle a t) (Rle t b)) (and (Rlt (Rabs (Rminus x t)) (pos (delta t))) (Rle (pos d) (pos (delta t))))) *)
exists t.
(* Goal: Rle v (pos (delta t)) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
repeat split ; apply Ht.
Qed.

Lemma compactness_value_2d :
  forall a b a' b' (delta : R -> R -> posreal),
  { d : posreal | forall x y, a <= x <= b -> a' <= y <= b' ->
    ~~ exists u, exists v, a <= u <= b /\ a' <= v <= b' /\ Rabs (x - u) < delta u v /\ Rabs (y - v) < delta u v /\ d <= delta u v }.
Proof.
(* Goal: forall (a b a' b' : R) (delta : forall (_ : R) (_ : R), posreal), @sig posreal (fun d : posreal => forall (x y : R) (_ : and (Rle a x) (Rle x b)) (_ : and (Rle a' y) (Rle y b')), not (not (@ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v))))))))))) *)
intros a b a' b' delta.
(* Goal: @sig posreal (fun d : posreal => forall (x y : R) (_ : and (Rle a x) (Rle x b)) (_ : and (Rle a' y) (Rle y b')), not (not (@ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v))))))))))) *)
destruct (compactness_value 2 (a,(a',tt)) (b,(b',tt)) (fun t => let '(u,(v,_)) := t in delta u v)) as (d, Hd).
(* Goal: @sig posreal (fun d : posreal => forall (x y : R) (_ : and (Rle a x) (Rle x b)) (_ : and (Rle a' y) (Rle y b')), not (not (@ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v))))))))))) *)
exists d.
(* Goal: forall (x y : R) (_ : and (Rle a x) (Rle x b)) (_ : and (Rle a' y) (Rle y b')), not (not (@ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v)))))))))) *)
intros x y Hx Hy.
(* Goal: not (not (@ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v)))))))))) *)
specialize (Hd (x,(y,tt)) (conj Hx (conj Hy I))).
(* Goal: not (not (@ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v)))))))))) *)
do 2 contradict Hd.
(* Goal: @ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v)))))))) *)
destruct Hd as ((u,(v,w)),Ht).
(* Goal: @ex R (fun u : R => @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v)))))))) *)
exists u.
(* Goal: @ex R (fun v : R => and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v))))))) *)
exists v.
(* Goal: and (and (Rle a u) (Rle u b)) (and (and (Rle a' v) (Rle v b')) (and (Rlt (Rabs (Rminus x u)) (pos (delta u v))) (and (Rlt (Rabs (Rminus y v)) (pos (delta u v))) (Rle (pos d) (pos (delta u v)))))) *)
simpl in Ht.
(* Goal: Rle v (pos (delta t)) *)
(* Goal: Rlt (Rdiv (@proj1_sig R (fun m : R => is_lub P m) d) (IZR (Zpos (xO xH)))) (@proj1_sig R (fun m : R => is_lub P m) (completeness P P2 P1)) *)
repeat split ; apply Ht.
Qed.
