(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
 
(*i $Id: Rtopology.v,v 1.1.2.1 2004/07/16 19:31:35 herbelin Exp $ i*)

Require Rbase.
Require Rfunctions.
Require Ranalysis1.
Require RList.
Require Classical_Prop.
Require Classical_Pred_Type.
V7only [Import R_scope.]. Open Local Scope R_scope.

Definition included [D1,D2:R->Prop] : Prop := (x:R)(D1 x)->(D2 x).
Definition disc [x:R;delta:posreal] : R->Prop := [y:R]``(Rabsolu (y-x))<delta``.
Definition neighbourhood [V:R->Prop;x:R] : Prop := (EXT delta:posreal | (included (disc x delta) V)).
Definition open_set [D:R->Prop] : Prop := (x:R) (D x)->(neighbourhood D x).
Definition complementary [D:R->Prop] : R->Prop := [c:R]~(D c).
Definition closed_set [D:R->Prop] : Prop := (open_set (complementary D)).
Definition intersection_domain [D1,D2:R->Prop] : R->Prop := [c:R](D1 c)/\(D2 c).
Definition union_domain [D1,D2:R->Prop] : R->Prop := [c:R](D1 c)\/(D2 c).
Definition interior [D:R->Prop] : R->Prop := [x:R](neighbourhood D x).

Lemma interior_P1 : (D:R->Prop) (included (interior D) D).
Intros; Unfold included; Unfold interior; Intros; Unfold neighbourhood in H; Elim H; Intros; Unfold included in H0; Apply H0; Unfold disc; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply (cond_pos x0).
Qed.

Lemma interior_P2 : (D:R->Prop) (open_set D) -> (included D (interior D)).
Intros; Unfold open_set in H; Unfold included; Intros; Assert H1 := (H ? H0); Unfold interior; Apply H1.
Qed.

Definition point_adherent [D:R->Prop;x:R] : Prop := (V:R->Prop) (neighbourhood V x) -> (EXT y:R | (intersection_domain V D y)).
Definition adherence [D:R->Prop] : R->Prop := [x:R](point_adherent D x).

Lemma adherence_P1 : (D:R->Prop) (included D (adherence D)).
Intro; Unfold included; Intros; Unfold adherence; Unfold point_adherent; Intros; Exists x; Unfold intersection_domain; Split.
Unfold neighbourhood in H0; Elim H0; Intros; Unfold included in H1; Apply H1; Unfold disc; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply (cond_pos x0).
Apply H.
Qed.

Lemma included_trans : (D1,D2,D3:R->Prop) (included D1 D2) -> (included D2 D3) -> (included D1 D3).
Unfold included; Intros; Apply H0; Apply H; Apply H1.
Qed.

Lemma interior_P3 : (D:R->Prop) (open_set (interior D)).
Intro; Unfold open_set interior; Unfold neighbourhood; Intros; Elim H; Intros.
Exists x0; Unfold included; Intros.
Pose del := ``x0-(Rabsolu (x-x1))``.
Cut ``0<del``.
Intro; Exists (mkposreal del H2); Intros.
Cut (included (disc x1 (mkposreal del H2)) (disc x x0)).
Intro; Assert H5 := (included_trans ? ? ? H4 H0).
Apply H5; Apply H3.
Unfold included; Unfold disc; Intros.
Apply Rle_lt_trans with ``(Rabsolu (x3-x1))+(Rabsolu (x1-x))``.
Replace ``x3-x`` with ``(x3-x1)+(x1-x)``; [Apply Rabsolu_triang | Ring].
Replace (pos x0) with ``del+(Rabsolu (x1-x))``.
Do 2 Rewrite <- (Rplus_sym (Rabsolu ``x1-x``)); Apply Rlt_compatibility; Apply H4.
Unfold del; Rewrite <- (Rabsolu_Ropp ``x-x1``); Rewrite Ropp_distr2; Ring.
Unfold del; Apply Rlt_anti_compatibility with ``(Rabsolu (x-x1))``; Rewrite Rplus_Or; Replace ``(Rabsolu (x-x1))+(x0-(Rabsolu (x-x1)))`` with (pos x0); [Idtac | Ring].
Unfold disc in H1; Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H1.
Qed.

Lemma complementary_P1 : (D:R->Prop) ~(EXT y:R | (intersection_domain D (complementary D) y)).
Intro; Red; Intro; Elim H; Intros; Unfold intersection_domain complementary in H0; Elim H0; Intros; Elim H2; Assumption.
Qed.

Lemma adherence_P2 : (D:R->Prop) (closed_set D) -> (included (adherence D) D).
Unfold closed_set; Unfold open_set complementary; Intros; Unfold included adherence; Intros; Assert H1 := (classic (D x)); Elim H1; Intro.
Assumption.
Assert H3 := (H ? H2); Assert H4 := (H0 ? H3); Elim H4; Intros; Unfold intersection_domain in H5; Elim H5; Intros; Elim H6; Assumption.
Qed.

Lemma adherence_P3 : (D:R->Prop) (closed_set (adherence D)).
Intro; Unfold closed_set adherence; Unfold open_set complementary point_adherent; Intros; Pose P := [V:R->Prop](neighbourhood V x)->(EXT y:R | (intersection_domain V D y)); Assert H0 := (not_all_ex_not ? P H); Elim H0; Intros V0 H1; Unfold P in H1; Assert H2 := (imply_to_and ? ? H1); Unfold neighbourhood; Elim H2; Intros; Unfold neighbourhood in H3; Elim H3; Intros; Exists x0; Unfold included; Intros; Red; Intro.
Assert H8 := (H7 V0); Cut (EXT delta:posreal | (x:R)(disc x1 delta x)->(V0 x)).
Intro; Assert H10 := (H8 H9); Elim H4; Assumption.
Cut ``0<x0-(Rabsolu (x-x1))``.
Intro; Pose del := (mkposreal ? H9); Exists del; Intros; Unfold included in H5; Apply H5; Unfold disc; Apply Rle_lt_trans with ``(Rabsolu (x2-x1))+(Rabsolu (x1-x))``.
Replace ``x2-x`` with ``(x2-x1)+(x1-x)``; [Apply Rabsolu_triang | Ring].
Replace (pos x0) with ``del+(Rabsolu (x1-x))``.
Do 2 Rewrite <- (Rplus_sym ``(Rabsolu (x1-x))``); Apply Rlt_compatibility; Apply H10.
Unfold del; Simpl; Rewrite <- (Rabsolu_Ropp ``x-x1``); Rewrite Ropp_distr2; Ring.
Apply Rlt_anti_compatibility with ``(Rabsolu (x-x1))``; Rewrite Rplus_Or; Replace ``(Rabsolu (x-x1))+(x0-(Rabsolu (x-x1)))`` with (pos x0); [Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H6 | Ring].
Qed.

Definition eq_Dom [D1,D2:R->Prop] : Prop := (included D1 D2)/\(included D2 D1).

Infix "=_D" eq_Dom (at level 5, no associativity).

Lemma open_set_P1 : (D:R->Prop) (open_set D) <-> D =_D (interior D).
Intro; Split.
Intro; Unfold eq_Dom; Split.
Apply interior_P2; Assumption.
Apply interior_P1.
Intro; Unfold eq_Dom in H; Elim H; Clear H; Intros; Unfold open_set; Intros; Unfold included interior in H; Unfold included in H0; Apply (H ? H1).
Qed.

Lemma closed_set_P1 : (D:R->Prop) (closed_set D) <-> D =_D (adherence D).
Intro; Split.
Intro; Unfold eq_Dom; Split.
Apply adherence_P1.
Apply adherence_P2; Assumption.
Unfold eq_Dom; Unfold included; Intros; Assert H0 := (adherence_P3 D); Unfold closed_set in H0; Unfold closed_set; Unfold open_set; Unfold open_set in H0; Intros; Assert H2 : (complementary (adherence D) x).
Unfold complementary; Unfold complementary in H1; Red; Intro; Elim H; Clear H; Intros _ H; Elim H1; Apply (H ? H2).
Assert H3 := (H0 ? H2); Unfold neighbourhood; Unfold neighbourhood in H3; Elim H3; Intros; Exists x0; Unfold included; Unfold included in H4; Intros; Assert H6 := (H4 ? H5); Unfold complementary in H6; Unfold complementary; Red; Intro; Elim H; Clear H; Intros H _; Elim H6; Apply (H ? H7).
Qed.

Lemma neighbourhood_P1 : (D1,D2:R->Prop;x:R) (included D1 D2) -> (neighbourhood D1 x) -> (neighbourhood D2 x).
Unfold included neighbourhood; Intros; Elim H0; Intros; Exists x0; Intros; Unfold included; Unfold included in H1; Intros; Apply (H ? (H1 ? H2)).
Qed.

Lemma open_set_P2 : (D1,D2:R->Prop) (open_set D1) -> (open_set D2) -> (open_set (union_domain D1 D2)).
Unfold open_set; Intros; Unfold union_domain in H1; Elim H1; Intro.
Apply neighbourhood_P1 with D1.
Unfold included union_domain; Tauto.
Apply H; Assumption.
Apply neighbourhood_P1 with D2.
Unfold included union_domain; Tauto.
Apply H0; Assumption.
Qed.

Lemma open_set_P3 : (D1,D2:R->Prop) (open_set D1) -> (open_set D2) -> (open_set (intersection_domain D1 D2)).
Unfold open_set; Intros; Unfold intersection_domain in H1; Elim H1; Intros.
Assert H4 := (H ? H2); Assert H5 := (H0 ? H3); Unfold intersection_domain; Unfold neighbourhood in H4 H5; Elim H4; Clear H; Intros del1 H; Elim H5; Clear H0; Intros del2 H0; Cut ``0<(Rmin del1 del2)``.
Intro; Pose del := (mkposreal ? H6).
Exists del; Unfold included; Intros; Unfold included in H H0; Unfold disc in H H0 H7.
Split.
Apply H; Apply Rlt_le_trans with (pos del).
Apply H7.
Unfold del; Simpl; Apply Rmin_l.
Apply H0; Apply Rlt_le_trans with (pos del).
Apply H7.
Unfold del; Simpl; Apply Rmin_r.
Unfold Rmin; Case (total_order_Rle del1 del2); Intro.
Apply (cond_pos del1).
Apply (cond_pos del2).
Qed.

Lemma open_set_P4 : (open_set [x:R]False).
Unfold open_set; Intros; Elim H.
Qed.

Lemma open_set_P5 : (open_set [x:R]True).
Unfold open_set; Intros; Unfold neighbourhood.
Exists (mkposreal R1 Rlt_R0_R1); Unfold included; Intros; Trivial.
Qed.

Lemma disc_P1 : (x:R;del:posreal) (open_set (disc x del)).
Intros; Assert H := (open_set_P1 (disc x del)).
Elim H; Intros; Apply H1.
Unfold eq_Dom; Split.
Unfold included interior disc; Intros; Cut ``0<del-(Rabsolu (x-x0))``.
Intro; Pose del2 := (mkposreal ? H3).
Exists del2; Unfold included; Intros.
Apply Rle_lt_trans with ``(Rabsolu (x1-x0))+(Rabsolu (x0 -x))``.
Replace ``x1-x`` with ``(x1-x0)+(x0-x)``; [Apply Rabsolu_triang | Ring].
Replace (pos del) with ``del2 + (Rabsolu (x0-x))``.
Do 2 Rewrite <- (Rplus_sym ``(Rabsolu (x0-x))``); Apply Rlt_compatibility.
Apply H4.
Unfold del2; Simpl; Rewrite <- (Rabsolu_Ropp ``x-x0``); Rewrite Ropp_distr2; Ring.
Apply Rlt_anti_compatibility with ``(Rabsolu (x-x0))``; Rewrite Rplus_Or; Replace ``(Rabsolu (x-x0))+(del-(Rabsolu (x-x0)))`` with (pos del); [Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H2 | Ring].
Apply interior_P1.
Qed.

Lemma continuity_P1 : (f:R->R;x:R) (continuity_pt f x) <-> (W:R->Prop)(neighbourhood W (f x)) -> (EXT V:R->Prop | (neighbourhood V x) /\ ((y:R)(V y)->(W (f y)))).
Intros; Split.
Intros; Unfold neighbourhood in H0.
Elim H0; Intros del1 H1.
Unfold continuity_pt in H; Unfold continue_in in H; Unfold limit1_in in H; Unfold limit_in in H; Simpl in H; Unfold R_dist in H.
Assert H2 := (H del1 (cond_pos del1)).
Elim H2; Intros del2 H3.
Elim H3; Intros.
Exists (disc x (mkposreal del2 H4)).
Intros; Unfold included in H1; Split.
Unfold neighbourhood disc.
Exists (mkposreal del2 H4).
Unfold included; Intros; Assumption.
Intros; Apply H1; Unfold disc; Case (Req_EM y x); Intro.
Rewrite H7; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply (cond_pos del1).
Apply H5; Split.
Unfold D_x no_cond; Split.
Trivial.
Apply not_sym; Apply H7.
Unfold disc in H6; Apply H6.
Intros; Unfold continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Intros.
Assert H1 := (H (disc (f x) (mkposreal eps H0))).
Cut (neighbourhood (disc (f x) (mkposreal eps H0)) (f x)).
Intro; Assert H3 := (H1 H2).
Elim H3; Intros D H4; Elim H4; Intros; Unfold neighbourhood in H5; Elim H5; Intros del1 H7.
Exists (pos del1); Split.
Apply (cond_pos del1).
Intros; Elim H8; Intros; Simpl in H10; Unfold R_dist in H10; Simpl; Unfold R_dist; Apply (H6 ? (H7 ? H10)).
Unfold neighbourhood disc; Exists (mkposreal eps H0); Unfold included; Intros; Assumption.
Qed.

Definition image_rec [f:R->R;D:R->Prop] : R->Prop := [x:R](D (f x)).

(**********)
Lemma continuity_P2 : (f:R->R;D:R->Prop) (continuity f) -> (open_set D) -> (open_set (image_rec f D)).
Intros; Unfold open_set in H0; Unfold open_set; Intros; Assert H2 := (continuity_P1 f x); Elim H2; Intros H3 _; Assert H4 := (H3 (H x)); Unfold neighbourhood image_rec; Unfold image_rec in H1; Assert H5 := (H4 D (H0 (f x) H1)); Elim H5; Intros V0 H6; Elim H6; Intros; Unfold neighbourhood in H7; Elim H7; Intros del H9; Exists del; Unfold included in H9; Unfold included; Intros; Apply (H8 ? (H9 ? H10)).
Qed.

(**********)
Lemma continuity_P3 : (f:R->R) (continuity f) <-> (D:R->Prop) (open_set D)->(open_set (image_rec f D)).
Intros; Split.
Intros; Apply continuity_P2; Assumption.
Intros; Unfold continuity; Unfold continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Cut (open_set (disc (f x) (mkposreal ? H0))).
Intro; Assert H2 := (H ? H1).
Unfold open_set image_rec in H2; Cut (disc (f x) (mkposreal ? H0) (f x)).
Intro; Assert H4 := (H2 ? H3).
Unfold neighbourhood in H4; Elim H4; Intros del H5.
Exists (pos del); Split.
Apply (cond_pos del).
Intros; Unfold included in H5; Apply H5; Elim H6; Intros; Apply H8.
Unfold disc; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply H0.
Apply disc_P1.
Qed.

(**********)
Theorem Rsepare : (x,y:R) ``x<>y``->(EXT V:R->Prop | (EXT W:R->Prop | (neighbourhood V x)/\(neighbourhood W y)/\~(EXT y:R | (intersection_domain V W y)))).
Intros x y Hsep; Pose D := ``(Rabsolu (x-y))``.
Cut ``0<D/2``.
Intro; Exists (disc x (mkposreal ? H)).
Exists (disc y (mkposreal ? H)); Split.
Unfold neighbourhood; Exists (mkposreal ? H); Unfold included; Tauto.
Split.
Unfold neighbourhood; Exists (mkposreal ? H); Unfold included; Tauto.
Red; Intro; Elim H0; Intros; Unfold intersection_domain in H1; Elim H1; Intros.
Cut ``D<D``.
Intro; Elim (Rlt_antirefl ? H4).
Change ``(Rabsolu (x-y))<D``; Apply Rle_lt_trans with ``(Rabsolu (x-x0))+(Rabsolu (x0-y))``.
Replace ``x-y`` with ``(x-x0)+(x0-y)``; [Apply Rabsolu_triang | Ring].
Rewrite (double_var D); Apply Rplus_lt.
Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H2.
Apply H3.
Unfold Rdiv; Apply Rmult_lt_pos.
Unfold D; Apply Rabsolu_pos_lt; Apply (Rminus_eq_contra ? ? Hsep).
Apply Rlt_Rinv; Sup0.
Qed.

Record family : Type := mkfamily {
  ind : R->Prop;
  f :> R->R->Prop;
  cond_fam : (x:R)(EXT y:R|(f x y))->(ind x) }.

Definition family_open_set [f:family] : Prop := (x:R) (open_set (f x)).

Definition domain_finite [D:R->Prop] : Prop := (EXT l:Rlist | (x:R)(D x)<->(In x l)).

Definition family_finite [f:family] : Prop := (domain_finite (ind f)).

Definition covering [D:R->Prop;f:family] : Prop := (x:R) (D x)->(EXT y:R | (f y x)).

Definition covering_open_set [D:R->Prop;f:family] : Prop := (covering D f)/\(family_open_set f).

Definition covering_finite [D:R->Prop;f:family] : Prop := (covering D f)/\(family_finite f).

Lemma restriction_family : (f:family;D:R->Prop) (x:R)(EXT y:R|([z1:R][z2:R](f z1 z2)/\(D z1) x y))->(intersection_domain (ind f) D x).
Intros; Elim H; Intros; Unfold intersection_domain; Elim H0; Intros; Split.
Apply (cond_fam f0); Exists x0; Assumption.
Assumption.
Qed.

Definition subfamily [f:family;D:R->Prop] : family := (mkfamily (intersection_domain (ind f) D) [x:R][y:R](f x y)/\(D x) (restriction_family f D)).

Definition compact [X:R->Prop] : Prop := (f:family) (covering_open_set X f) -> (EXT D:R->Prop | (covering_finite X (subfamily f D))).

(**********)
Lemma family_P1 : (f:family;D:R->Prop) (family_open_set f) -> (family_open_set (subfamily f D)).
Unfold family_open_set; Intros; Unfold subfamily; Simpl; Assert H0 := (classic (D x)).
Elim H0; Intro.
Cut (open_set (f0 x))->(open_set [y:R](f0 x y)/\(D x)).
Intro; Apply H2; Apply H.
Unfold open_set; Unfold neighbourhood; Intros; Elim H3; Intros; Assert H6 := (H2 ? H4); Elim H6; Intros; Exists x1; Unfold included; Intros; Split.
Apply (H7 ? H8).
Assumption.
Cut (open_set [y:R]False) -> (open_set [y:R](f0 x y)/\(D x)).
Intro; Apply H2; Apply open_set_P4.
Unfold open_set; Unfold neighbourhood; Intros; Elim H3; Intros; Elim H1; Assumption.
Qed.

Definition bounded [D:R->Prop] : Prop := (EXT m:R | (EXT M:R | (x:R)(D x)->``m<=x<=M``)).

Lemma open_set_P6 : (D1,D2:R->Prop) (open_set D1) -> D1 =_D D2 -> (open_set D2).
Unfold open_set; Unfold neighbourhood; Intros.
Unfold eq_Dom in H0; Elim H0; Intros.
Assert H4 := (H ? (H3 ? H1)).
Elim H4; Intros.
Exists x0; Apply included_trans with D1; Assumption.
Qed.

(**********)
Lemma compact_P1 : (X:R->Prop) (compact X) -> (bounded X).
Intros; Unfold compact in H; Pose D := [x:R]True; Pose g := [x:R][y:R]``(Rabsolu y)<x``; Cut (x:R)(EXT y|(g x y))->True; [Intro | Intro; Trivial].
Pose f0 := (mkfamily D g H0); Assert H1 := (H f0); Cut (covering_open_set X f0).
Intro; Assert H3 := (H1 H2); Elim H3; Intros D' H4; Unfold covering_finite in H4; Elim H4; Intros; Unfold family_finite in H6; Unfold domain_finite in H6; Elim H6; Intros l H7; Unfold bounded; Pose r := (MaxRlist l).
Exists ``-r``; Exists r; Intros.
Unfold covering in H5; Assert H9 := (H5 ? H8); Elim H9; Intros; Unfold subfamily in H10; Simpl in H10; Elim H10; Intros; Assert H13 := (H7 x0); Simpl in H13; Cut (intersection_domain D D' x0).
Elim H13; Clear H13; Intros.
Assert H16 := (H13 H15); Unfold g in H11; Split.
Cut ``x0<=r``.
Intro; Cut ``(Rabsolu x)<r``.
Intro; Assert H19 := (Rabsolu_def2 x r H18); Elim H19; Intros; Left; Assumption.
Apply Rlt_le_trans with x0; Assumption.
Apply (MaxRlist_P1 l x0 H16).
Cut ``x0<=r``.
Intro; Apply Rle_trans with (Rabsolu x).
Apply Rle_Rabsolu.
Apply Rle_trans with x0.
Left; Apply H11.
Assumption.
Apply (MaxRlist_P1 l x0 H16).
Unfold intersection_domain D; Tauto.
Unfold covering_open_set; Split.
Unfold covering; Intros; Simpl; Exists ``(Rabsolu x)+1``; Unfold g; Pattern 1 (Rabsolu x); Rewrite <- Rplus_Or; Apply Rlt_compatibility; Apply Rlt_R0_R1.
Unfold family_open_set; Intro; Case (total_order R0 x); Intro.
Apply open_set_P6 with (disc R0 (mkposreal ? H2)).
Apply disc_P1.
Unfold eq_Dom; Unfold f0; Simpl; Unfold g disc; Split.
Unfold included; Intros; Unfold Rminus in H3; Rewrite Ropp_O in H3; Rewrite Rplus_Or in H3; Apply H3.
Unfold included; Intros; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Apply H3.
Apply open_set_P6 with [x:R]False.
Apply open_set_P4.
Unfold eq_Dom; Split.
Unfold included; Intros; Elim H3.
Unfold included f0; Simpl; Unfold g; Intros; Elim H2; Intro; [Rewrite <- H4 in H3; Assert H5 := (Rabsolu_pos x0); Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H5 H3)) | Assert H6 := (Rabsolu_pos x0); Assert H7 := (Rlt_trans ? ? ? H3 H4); Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H6 H7))].
Qed.

(**********)
Lemma compact_P2 : (X:R->Prop) (compact X) -> (closed_set X).
Intros; Assert H0 := (closed_set_P1 X); Elim H0; Clear H0; Intros _ H0; Apply H0; Clear H0.
Unfold eq_Dom; Split.
Apply adherence_P1.
Unfold included; Unfold adherence; Unfold point_adherent; Intros; Unfold compact in H; Assert H1 := (classic (X x)); Elim H1; Clear H1; Intro.
Assumption.
Cut (y:R)(X y)->``0<(Rabsolu (y-x))/2``.
Intro; Pose D := X; Pose g := [y:R][z:R]``(Rabsolu (y-z))<(Rabsolu (y-x))/2``/\(D y); Cut (x:R)(EXT y|(g x y))->(D x).
Intro; Pose f0 := (mkfamily D g H3); Assert H4 := (H f0); Cut (covering_open_set X f0).
Intro; Assert H6 := (H4 H5); Elim H6; Clear H6; Intros D' H6.
Unfold covering_finite in H6; Decompose [and] H6; Unfold covering subfamily in H7; Simpl in H7; Unfold family_finite subfamily in H8; Simpl in H8; Unfold domain_finite in H8; Elim H8; Clear H8; Intros l H8; Pose alp := (MinRlist (AbsList l x)); Cut ``0<alp``.
Intro; Assert H10 := (H0 (disc x (mkposreal ? H9))); Cut (neighbourhood (disc x (mkposreal alp H9)) x).
Intro; Assert H12 := (H10 H11); Elim H12; Clear H12; Intros y H12; Unfold intersection_domain in H12; Elim H12; Clear H12; Intros; Assert H14 := (H7 ? H13); Elim H14; Clear H14; Intros y0 H14; Elim H14; Clear H14; Intros; Unfold g in H14; Elim H14; Clear H14; Intros; Unfold disc in H12; Simpl in H12; Cut ``alp<=(Rabsolu (y0-x))/2``.
Intro; Assert H18 := (Rlt_le_trans ? ? ? H12 H17); Cut ``(Rabsolu (y0-x))<(Rabsolu (y0-x))``.
Intro; Elim (Rlt_antirefl ? H19).
Apply Rle_lt_trans with ``(Rabsolu (y0-y))+(Rabsolu (y-x))``.
Replace ``y0-x`` with ``(y0-y)+(y-x)``; [Apply Rabsolu_triang | Ring].
Rewrite (double_var ``(Rabsolu (y0-x))``); Apply Rplus_lt; Assumption.
Apply (MinRlist_P1 (AbsList l x) ``(Rabsolu (y0-x))/2``); Apply AbsList_P1; Elim (H8 y0); Clear H8; Intros; Apply H8; Unfold intersection_domain; Split; Assumption.
Assert H11 := (disc_P1 x (mkposreal alp H9)); Unfold open_set in H11; Apply H11.
Unfold disc; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply H9.
Unfold alp; Apply MinRlist_P2; Intros; Assert H10 := (AbsList_P2 ? ? ? H9); Elim H10; Clear H10; Intros z H10; Elim H10; Clear H10; Intros; Rewrite H11; Apply H2; Elim (H8 z); Clear H8; Intros; Assert H13 := (H12 H10); Unfold intersection_domain D in H13; Elim H13; Clear H13; Intros; Assumption.
Unfold covering_open_set; Split.
Unfold covering; Intros; Exists x0; Simpl; Unfold g; Split.
Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Unfold Rminus in H2; Apply (H2 ? H5).
Apply H5.
Unfold family_open_set; Intro; Simpl; Unfold g; Elim (classic (D x0)); Intro.
Apply open_set_P6 with (disc x0 (mkposreal ? (H2 ? H5))).
Apply disc_P1.
Unfold eq_Dom; Split.
Unfold included disc; Simpl; Intros; Split.
Rewrite <- (Rabsolu_Ropp ``x0-x1``); Rewrite Ropp_distr2; Apply H6.
Apply H5.
Unfold included disc; Simpl; Intros; Elim H6; Intros; Rewrite <- (Rabsolu_Ropp ``x1-x0``); Rewrite Ropp_distr2; Apply H7.
Apply open_set_P6 with [z:R]False.
Apply open_set_P4.
Unfold eq_Dom; Split.
Unfold included; Intros; Elim H6.
Unfold included; Intros; Elim H6; Intros; Elim H5; Assumption.
Intros; Elim H3; Intros; Unfold g in H4; Elim H4; Clear H4; Intros _ H4; Apply H4.
Intros; Unfold Rdiv; Apply Rmult_lt_pos.
Apply Rabsolu_pos_lt; Apply Rminus_eq_contra; Red; Intro; Rewrite H3 in H2; Elim H1; Apply H2.
Apply Rlt_Rinv; Sup0.
Qed.

(**********)
Lemma compact_EMP : (compact [_:R]False).
Unfold compact; Intros; Exists [x:R]False; Unfold covering_finite; Split.
Unfold covering; Intros; Elim H0.
Unfold family_finite; Unfold domain_finite; Exists nil; Intro.
Split.
Simpl; Unfold intersection_domain; Intros; Elim H0.
Elim H0; Clear H0; Intros _ H0; Elim H0.
Simpl; Intro; Elim H0.
Qed.

Lemma compact_eqDom : (X1,X2:R->Prop) (compact X1) -> X1 =_D X2 -> (compact X2).
Unfold compact; Intros; Unfold eq_Dom in H0; Elim H0; Clear H0; Unfold included; Intros; Assert H3 : (covering_open_set X1 f0).
Unfold covering_open_set; Unfold covering_open_set in H1; Elim H1; Clear H1; Intros; Split.
Unfold covering in H1; Unfold covering; Intros; Apply (H1 ? (H0 ? H4)).
Apply H3.
Elim (H ? H3); Intros D H4; Exists D; Unfold covering_finite; Unfold covering_finite in H4; Elim H4; Intros; Split.
Unfold covering in H5; Unfold covering; Intros; Apply (H5 ? (H2 ? H7)).
Apply H6.
Qed.

(* Borel-Lebesgue's lemma *)
Lemma compact_P3 : (a,b:R) (compact [c:R]``a<=c<=b``).
Intros; Case (total_order_Rle a b); Intro.
Unfold compact; Intros; Pose A := [x:R]``a<=x<=b``/\(EXT D:R->Prop | (covering_finite [c:R]``a <= c <= x`` (subfamily f0 D))); Cut (A a).
Intro; Cut (bound A).
Intro; Cut (EXT a0:R | (A a0)).
Intro; Assert H3 := (complet A H1 H2); Elim H3; Clear H3; Intros m H3; Unfold is_lub in H3; Cut ``a<=m<=b``.
Intro; Unfold covering_open_set in H; Elim H; Clear H; Intros; Unfold covering in H; Assert H6 := (H m H4); Elim H6; Clear H6; Intros y0 H6; Unfold family_open_set in H5; Assert H7 := (H5 y0); Unfold open_set in H7; Assert H8 := (H7 m H6); Unfold neighbourhood in H8; Elim H8; Clear H8; Intros eps H8; Cut (EXT x:R | (A x)/\``m-eps<x<=m``).
Intro; Elim H9; Clear H9; Intros x H9; Elim H9; Clear H9; Intros; Case (Req_EM m b); Intro.
Rewrite H11 in H10; Rewrite H11 in H8; Unfold A in H9; Elim H9; Clear H9; Intros; Elim H12; Clear H12; Intros Dx H12; Pose Db := [x:R](Dx x)\/x==y0; Exists Db; Unfold covering_finite; Split.
Unfold covering; Unfold covering_finite in H12; Elim H12; Clear H12; Intros; Unfold covering in H12; Case (total_order_Rle x0 x); Intro.
Cut ``a<=x0<=x``.
Intro; Assert H16 := (H12 x0 H15); Elim H16; Clear H16; Intros; Exists x1; Simpl in H16; Simpl; Unfold Db; Elim H16; Clear H16; Intros; Split; [Apply H16 | Left; Apply H17].
Split.
Elim H14; Intros; Assumption.
Assumption.
Exists y0; Simpl; Split.
Apply H8; Unfold disc; Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Rewrite Rabsolu_right.
Apply Rlt_trans with ``b-x``.
Unfold Rminus; Apply Rlt_compatibility; Apply Rlt_Ropp; Auto with real.
Elim H10; Intros H15 _; Apply Rlt_anti_compatibility with ``x-eps``; Replace ``x-eps+(b-x)`` with ``b-eps``; [Replace ``x-eps+eps`` with x; [Apply H15 | Ring] | Ring].
Apply Rge_minus; Apply Rle_sym1; Elim H14; Intros _ H15; Apply H15.
Unfold Db; Right; Reflexivity.
Unfold family_finite; Unfold domain_finite; Unfold covering_finite in H12; Elim H12; Clear H12; Intros; Unfold family_finite in H13; Unfold domain_finite in H13; Elim H13; Clear H13; Intros l H13; Exists (cons y0 l); Intro; Split.
Intro; Simpl in H14; Unfold intersection_domain in H14; Elim (H13 x0); Clear H13; Intros; Case (Req_EM x0 y0); Intro.
Simpl; Left; Apply H16.
Simpl; Right; Apply H13.
Simpl; Unfold intersection_domain; Unfold Db in H14; Decompose [and or] H14.
Split; Assumption.
Elim H16; Assumption.
Intro; Simpl in H14; Elim H14; Intro; Simpl; Unfold intersection_domain.
Split.
Apply (cond_fam f0); Rewrite H15; Exists m; Apply H6.
Unfold Db; Right; Assumption.
Simpl; Unfold intersection_domain; Elim (H13 x0).
Intros _ H16; Assert H17 := (H16 H15); Simpl in H17; Unfold intersection_domain in H17; Split.
Elim H17; Intros; Assumption.
Unfold Db; Left; Elim H17; Intros; Assumption.
Pose m' := (Rmin ``m+eps/2`` b); Cut (A m').
Intro; Elim H3; Intros; Unfold is_upper_bound in H13; Assert H15 := (H13 m' H12); Cut ``m<m'``.
Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H15 H16)).
Unfold m'; Unfold Rmin; Case (total_order_Rle ``m+eps/2`` b); Intro.
Pattern 1 m; Rewrite <- Rplus_Or; Apply Rlt_compatibility; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos eps) | Apply Rlt_Rinv; Sup0].
Elim H4; Intros.
Elim H17; Intro.
Assumption.
Elim H11; Assumption.
Unfold A; Split.
Split.
Apply Rle_trans with m.
Elim H4; Intros; Assumption.
Unfold m'; Unfold Rmin; Case (total_order_Rle ``m+eps/2`` b); Intro.
Pattern 1 m; Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos eps) | Apply Rlt_Rinv; Sup0].
Elim H4; Intros.
Elim H13; Intro.
Assumption.
Elim H11; Assumption.
Unfold m'; Apply Rmin_r.
Unfold A in H9; Elim H9; Clear H9; Intros; Elim H12; Clear H12; Intros Dx H12; Pose Db := [x:R](Dx x)\/x==y0; Exists Db; Unfold covering_finite; Split.
Unfold covering; Unfold covering_finite in H12; Elim H12; Clear H12; Intros; Unfold covering in H12; Case (total_order_Rle x0 x); Intro.
Cut ``a<=x0<=x``.
Intro; Assert H16 := (H12 x0 H15); Elim H16; Clear H16; Intros; Exists x1; Simpl in H16; Simpl; Unfold Db.
Elim H16; Clear H16; Intros; Split; [Apply H16 | Left; Apply H17].
Elim H14; Intros; Split; Assumption.
Exists y0; Simpl; Split.
Apply H8; Unfold disc; Unfold Rabsolu; Case (case_Rabsolu ``x0-m``); Intro.
Rewrite Ropp_distr2; Apply Rlt_trans with ``m-x``.
Unfold Rminus; Apply Rlt_compatibility; Apply Rlt_Ropp; Auto with real.
Apply Rlt_anti_compatibility with ``x-eps``; Replace ``x-eps+(m-x)`` with ``m-eps``.
Replace ``x-eps+eps`` with x.
Elim H10; Intros; Assumption.
Ring.
Ring.
Apply Rle_lt_trans with ``m'-m``.
Unfold Rminus; Do 2 Rewrite <- (Rplus_sym ``-m``); Apply Rle_compatibility; Elim H14; Intros; Assumption.
Apply Rlt_anti_compatibility with m; Replace ``m+(m'-m)`` with m'.
Apply Rle_lt_trans with ``m+eps/2``.
Unfold m'; Apply Rmin_l.
Apply Rlt_compatibility; Apply Rlt_monotony_contra with ``2``.
Sup0.
Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
Rewrite Rmult_1l; Pattern 1 (pos eps); Rewrite <- Rplus_Or; Rewrite double; Apply Rlt_compatibility; Apply (cond_pos eps).
DiscrR.
Ring.
Unfold Db; Right; Reflexivity.
Unfold family_finite; Unfold domain_finite; Unfold covering_finite in H12; Elim H12; Clear H12; Intros; Unfold family_finite in H13; Unfold domain_finite in H13; Elim H13; Clear H13; Intros l H13; Exists (cons y0 l); Intro; Split.
Intro; Simpl in H14; Unfold intersection_domain in H14; Elim (H13 x0); Clear H13; Intros; Case (Req_EM x0 y0); Intro.
Simpl; Left; Apply H16.
Simpl; Right; Apply H13; Simpl; Unfold intersection_domain; Unfold Db in H14; Decompose [and or] H14.
Split; Assumption.
Elim H16; Assumption.
Intro; Simpl in H14; Elim H14; Intro; Simpl; Unfold intersection_domain.
Split.
Apply (cond_fam f0); Rewrite H15; Exists m; Apply H6.
Unfold Db; Right; Assumption.
Elim (H13 x0); Intros _ H16.
Assert H17 := (H16 H15).
Simpl in H17.
Unfold intersection_domain in H17.
Split.
Elim H17; Intros; Assumption.
Unfold Db; Left; Elim H17; Intros; Assumption.
Elim (classic (EXT x:R | (A x)/\``m-eps < x <= m``)); Intro.
Assumption.
Elim H3; Intros; Cut (is_upper_bound A ``m-eps``).
Intro; Assert H13 := (H11 ? H12); Cut ``m-eps<m``.
Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H13 H14)).
Pattern 2 m; Rewrite <- Rplus_Or; Unfold Rminus; Apply Rlt_compatibility; Apply Ropp_Rlt; Rewrite Ropp_Ropp; Rewrite Ropp_O; Apply (cond_pos eps).
Pose P := [n:R](A n)/\``m-eps<n<=m``; Assert H12 := (not_ex_all_not ? P H9); Unfold P in H12; Unfold is_upper_bound; Intros; Assert H14 := (not_and_or ? ? (H12 x)); Elim H14; Intro.
Elim H15; Apply H13.
Elim (not_and_or ? ? H15); Intro.
Case (total_order_Rle x ``m-eps``); Intro.
Assumption.
Elim H16; Auto with real.
Unfold is_upper_bound in H10; Assert H17 := (H10 x H13); Elim H16; Apply H17.
Elim H3; Clear H3; Intros.
Unfold is_upper_bound in H3.
Split.
Apply (H3 ? H0).
Apply (H4 b); Unfold is_upper_bound; Intros; Unfold A in H5; Elim H5; Clear H5; Intros H5 _; Elim H5; Clear H5; Intros _ H5; Apply H5.
Exists a; Apply H0.
Unfold bound; Exists b; Unfold is_upper_bound; Intros; Unfold A in H1; Elim H1; Clear H1; Intros H1 _; Elim H1; Clear H1; Intros _ H1; Apply H1.
Unfold A; Split.
Split; [Right; Reflexivity | Apply r].
Unfold covering_open_set in H; Elim H; Clear H; Intros; Unfold covering in H; Cut ``a<=a<=b``.
Intro; Elim (H ? H1); Intros y0 H2; Pose D':=[x:R]x==y0; Exists D'; Unfold covering_finite; Split.
Unfold covering; Simpl; Intros; Cut x==a.
Intro; Exists y0; Split.
Rewrite H4; Apply H2.
Unfold D'; Reflexivity.
Elim H3; Intros; Apply Rle_antisym; Assumption.
Unfold family_finite; Unfold domain_finite; Exists (cons y0 nil); Intro; Split.
Simpl; Unfold intersection_domain; Intro; Elim H3; Clear H3; Intros; Unfold D' in H4; Left; Apply H4.
Simpl; Unfold intersection_domain; Intro; Elim H3; Intro.
Split; [Rewrite H4; Apply (cond_fam f0); Exists a; Apply H2 | Apply H4].
Elim H4.
Split; [Right; Reflexivity | Apply r].
Apply compact_eqDom with [c:R]False.
Apply compact_EMP.
Unfold eq_Dom; Split.
Unfold included; Intros; Elim H.
Unfold included; Intros; Elim H; Clear H; Intros; Assert H1 := (Rle_trans ? ? ? H H0); Elim n; Apply H1.
Qed.

Lemma compact_P4 : (X,F:R->Prop) (compact X) -> (closed_set F) -> (included F X) -> (compact F).
Unfold compact; Intros; Elim (classic (EXT z:R | (F z))); Intro Hyp_F_NE.
Pose D := (ind f0); Pose g := (f f0); Unfold closed_set in H0.
Pose g' := [x:R][y:R](f0 x y)\/((complementary F y)/\(D x)).
Pose D' := D.
Cut (x:R)(EXT y:R | (g' x y))->(D' x).
Intro; Pose f' := (mkfamily D' g' H3); Cut (covering_open_set X f').
Intro; Elim (H ? H4); Intros DX H5; Exists DX.
Unfold covering_finite; Unfold covering_finite in H5; Elim H5; Clear H5; Intros.
Split.
Unfold covering; Unfold covering in H5; Intros.
Elim (H5 ? (H1 ? H7)); Intros y0 H8; Exists y0; Simpl in H8; Simpl; Elim H8; Clear H8; Intros.
Split.
Unfold g' in H8; Elim H8; Intro.
Apply H10.
Elim H10; Intros H11 _; Unfold complementary in H11; Elim H11; Apply H7.
Apply H9.
Unfold family_finite; Unfold domain_finite; Unfold family_finite in H6; Unfold domain_finite in H6; Elim H6; Clear H6; Intros l H6; Exists l; Intro; Assert H7 := (H6 x); Elim H7; Clear H7; Intros.
Split.
Intro; Apply H7; Simpl; Unfold intersection_domain; Simpl in H9; Unfold intersection_domain in H9; Unfold D'; Apply H9.
Intro; Assert H10 := (H8 H9); Simpl in H10; Unfold intersection_domain in H10; Simpl; Unfold intersection_domain; Unfold D' in H10; Apply H10.
Unfold covering_open_set; Unfold covering_open_set in H2; Elim H2; Clear H2; Intros.
Split.
Unfold covering; Unfold covering in H2; Intros.
Elim (classic (F x)); Intro.
Elim (H2 ? H6); Intros y0 H7; Exists y0; Simpl; Unfold g'; Left; Assumption.
Cut (EXT z:R | (D z)).
Intro; Elim H7; Clear H7; Intros x0 H7; Exists x0; Simpl; Unfold g'; Right.
Split.
Unfold complementary; Apply H6.
Apply H7.
Elim Hyp_F_NE; Intros z0 H7.
Assert H8 := (H2 ? H7).
Elim H8; Clear H8; Intros t H8; Exists t; Apply (cond_fam f0); Exists z0; Apply H8.
Unfold family_open_set; Intro; Simpl; Unfold g'; Elim (classic (D x)); Intro.
Apply open_set_P6 with (union_domain (f0 x) (complementary F)).
Apply open_set_P2.
Unfold family_open_set in H4; Apply H4.
Apply H0.
Unfold eq_Dom; Split.
Unfold included union_domain complementary; Intros.
Elim H6; Intro; [Left; Apply H7 | Right; Split; Assumption].
Unfold included union_domain complementary; Intros.
Elim H6; Intro; [Left; Apply H7 | Right; Elim H7; Intros; Apply H8].
Apply open_set_P6 with (f0 x).
Unfold family_open_set in H4; Apply H4.
Unfold eq_Dom; Split.
Unfold included complementary; Intros; Left; Apply H6.
Unfold included complementary; Intros.
Elim H6; Intro.
Apply H7.
Elim H7; Intros _ H8; Elim H5; Apply H8.
Intros; Elim H3; Intros y0 H4; Unfold g' in H4; Elim H4; Intro.
Apply (cond_fam f0); Exists y0; Apply H5.
Elim H5; Clear H5; Intros _ H5; Apply H5.
(* Cas ou F est l'ensemble vide *)
Cut (compact F).
Intro; Apply (H3 f0 H2).
Apply compact_eqDom with [_:R]False.
Apply compact_EMP.
Unfold eq_Dom; Split.
Unfold included; Intros; Elim H3.
Assert H3 := (not_ex_all_not ? ? Hyp_F_NE); Unfold included; Intros; Elim (H3 x); Apply H4.
Qed.

(**********)
Lemma compact_P5 : (X:R->Prop) (closed_set X)->(bounded X)->(compact X).
Intros; Unfold bounded in H0.
Elim H0; Clear H0; Intros m H0.
Elim H0; Clear H0; Intros M H0.
Assert H1 := (compact_P3 m M).
Apply (compact_P4 [c:R]``m<=c<=M`` X H1 H H0).
Qed.

(**********)
Lemma compact_carac : (X:R->Prop) (compact X)<->(closed_set X)/\(bounded X).
Intro; Split.
Intro; Split; [Apply (compact_P2 ? H) | Apply (compact_P1 ? H)].
Intro; Elim H; Clear H; Intros; Apply (compact_P5 ? H H0).
Qed.

Definition image_dir [f:R->R;D:R->Prop] : R->Prop := [x:R](EXT y:R | x==(f y)/\(D y)).

(**********)
Lemma continuity_compact : (f:R->R;X:R->Prop) ((x:R)(continuity_pt f x)) -> (compact X) -> (compact (image_dir f X)).
Unfold compact; Intros; Unfold covering_open_set in H1.
Elim H1; Clear H1; Intros.
Pose D := (ind f1).
Pose g := [x:R][y:R](image_rec f0 (f1 x) y).
Cut (x:R)(EXT y:R | (g x y))->(D x).
Intro; Pose f' := (mkfamily D g H3).
Cut (covering_open_set X f').
Intro; Elim (H0 f' H4); Intros D' H5; Exists D'.
Unfold covering_finite in H5; Elim H5; Clear H5; Intros; Unfold covering_finite; Split.
Unfold covering image_dir; Simpl; Unfold covering in H5; Intros; Elim H7; Intros y H8; Elim H8; Intros; Assert H11 := (H5 ? H10); Simpl in H11; Elim H11; Intros z H12; Exists z; Unfold g in H12; Unfold image_rec in H12; Rewrite H9; Apply H12.
Unfold family_finite in H6; Unfold domain_finite in H6; Unfold family_finite; Unfold domain_finite; Elim H6; Intros l H7; Exists l; Intro; Elim (H7 x); Intros; Split; Intro.
Apply H8; Simpl in H10; Simpl; Apply H10.
Apply (H9 H10).
Unfold covering_open_set; Split.
Unfold covering; Intros; Simpl; Unfold covering in H1; Unfold image_dir in H1; Unfold g; Unfold image_rec; Apply H1.
Exists x; Split; [Reflexivity | Apply H4].
Unfold family_open_set; Unfold family_open_set in H2; Intro; Simpl; Unfold g; Cut ([y:R](image_rec f0 (f1 x) y))==(image_rec f0 (f1 x)).
Intro; Rewrite H4.
Apply (continuity_P2 f0 (f1 x) H (H2 x)).
Reflexivity.
Intros; Apply (cond_fam f1); Unfold g in H3; Unfold image_rec in H3; Elim H3; Intros; Exists (f0 x0); Apply H4.
Qed.

Lemma Rlt_Rminus : (a,b:R) ``a<b`` -> ``0<b-a``.
Intros; Apply Rlt_anti_compatibility with a; Rewrite Rplus_Or; Replace ``a+(b-a)`` with b; [Assumption | Ring].
Qed.

Lemma prolongement_C0 : (f:R->R;a,b:R) ``a<=b`` -> ((c:R)``a<=c<=b``->(continuity_pt f c)) -> (EXT g:R->R | (continuity g)/\((c:R)``a<=c<=b``->(g c)==(f c))).
Intros; Elim H; Intro.
Pose h := [x:R](Cases (total_order_Rle x a) of
  (leftT _) => (f0 a)
| (rightT _) => (Cases (total_order_Rle x b) of
       (leftT _) => (f0 x)
     | (rightT _) => (f0 b) end) end).
Assert H2 : ``0<b-a``.
Apply Rlt_Rminus; Assumption.
Exists h; Split.
Unfold continuity; Intro; Case (total_order x a); Intro.
Unfold continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Exists ``a-x``; Split.
Change ``0<a-x``; Apply Rlt_Rminus; Assumption.
Intros; Elim H5; Clear H5; Intros _ H5; Unfold h.
Case (total_order_Rle x a); Intro.
Case (total_order_Rle x0 a); Intro.
Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
Elim n; Left; Apply Rlt_anti_compatibility with ``-x``; Do 2 Rewrite (Rplus_sym ``-x``); Apply Rle_lt_trans with ``(Rabsolu (x0-x))``.
Apply Rle_Rabsolu.
Assumption.
Elim n; Left; Assumption.
Elim H3; Intro.
Assert H5 : ``a<=a<=b``.
Split; [Right; Reflexivity | Left; Assumption].
Assert H6 := (H0 ? H5); Unfold continuity_pt in H6; Unfold continue_in in H6; Unfold limit1_in in H6; Unfold limit_in in H6; Simpl in H6; Unfold R_dist in H6; Unfold continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H6 ? H7); Intros; Exists (Rmin x0 ``b-a``); Split.
Unfold Rmin; Case (total_order_Rle x0 ``b-a``); Intro.
Elim H8; Intros; Assumption.
Change ``0<b-a``; Apply Rlt_Rminus; Assumption.
Intros; Elim H9; Clear H9; Intros _ H9; Cut ``x1<b``.
Intro; Unfold h; Case (total_order_Rle x a); Intro.
Case (total_order_Rle x1 a); Intro.
Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
Case (total_order_Rle x1 b); Intro.
Elim H8; Intros; Apply H12; Split.
Unfold D_x no_cond; Split.
Trivial.
Red; Intro; Elim n; Right; Symmetry; Assumption.
Apply Rlt_le_trans with (Rmin x0 ``b-a``).
Rewrite H4 in H9; Apply H9.
Apply Rmin_l.
Elim n0; Left; Assumption.
Elim n; Right; Assumption.
Apply Rlt_anti_compatibility with ``-a``; Do 2 Rewrite (Rplus_sym ``-a``); Rewrite H4 in H9; Apply Rle_lt_trans with ``(Rabsolu (x1-a))``.
Apply Rle_Rabsolu.
Apply Rlt_le_trans with ``(Rmin x0 (b-a))``.
Assumption.
Apply Rmin_r.
Case (total_order x b); Intro.
Assert H6 : ``a<=x<=b``.
Split; Left; Assumption.
Assert H7 := (H0 ? H6); Unfold continuity_pt in H7; Unfold continue_in in H7; Unfold limit1_in in H7; Unfold limit_in in H7; Simpl in H7; Unfold R_dist in H7; Unfold continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H7 ? H8); Intros; Elim H9; Clear H9; Intros.
Assert H11 : ``0<x-a``.
Apply Rlt_Rminus; Assumption.
Assert H12 : ``0<b-x``.
Apply Rlt_Rminus; Assumption.
Exists (Rmin x0 (Rmin ``x-a`` ``b-x``)); Split.
Unfold Rmin; Case (total_order_Rle ``x-a`` ``b-x``); Intro.
Case (total_order_Rle x0 ``x-a``); Intro.
Assumption.
Assumption.
Case (total_order_Rle x0 ``b-x``); Intro.
Assumption.
Assumption.
Intros; Elim H13; Clear H13; Intros; Cut ``a<x1<b``.
Intro; Elim H15; Clear H15; Intros; Unfold h; Case (total_order_Rle x a); Intro.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H4)).
Case (total_order_Rle x b); Intro.
Case (total_order_Rle x1 a); Intro.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r0 H15)).
Case (total_order_Rle x1 b); Intro.
Apply H10; Split.
Assumption.
Apply Rlt_le_trans with ``(Rmin x0 (Rmin (x-a) (b-x)))``.
Assumption.
Apply Rmin_l.
Elim n1; Left; Assumption.
Elim n0; Left; Assumption.
Split.
Apply Ropp_Rlt; Apply Rlt_anti_compatibility with x; Apply Rle_lt_trans with ``(Rabsolu (x1-x))``.
Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply Rle_Rabsolu.
Apply Rlt_le_trans with ``(Rmin x0 (Rmin (x-a) (b-x)))``.
Assumption.
Apply Rle_trans with ``(Rmin (x-a) (b-x))``.
Apply Rmin_r.
Apply Rmin_l.
Apply Rlt_anti_compatibility with ``-x``; Do 2 Rewrite (Rplus_sym ``-x``); Apply Rle_lt_trans with ``(Rabsolu (x1-x))``.
Apply Rle_Rabsolu.
Apply Rlt_le_trans with ``(Rmin x0 (Rmin (x-a) (b-x)))``.
Assumption.
Apply Rle_trans with ``(Rmin (x-a) (b-x))``; Apply Rmin_r.
Elim H5; Intro.
Assert H7 : ``a<=b<=b``.
Split; [Left; Assumption | Right; Reflexivity].
Assert H8 := (H0 ? H7); Unfold continuity_pt in H8; Unfold continue_in in H8; Unfold limit1_in in H8; Unfold limit_in in H8; Simpl in H8; Unfold R_dist in H8; Unfold continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H8 ? H9); Intros; Exists (Rmin x0 ``b-a``); Split.
Unfold Rmin; Case (total_order_Rle x0 ``b-a``); Intro.
Elim H10; Intros; Assumption.
Change ``0<b-a``; Apply Rlt_Rminus; Assumption.
Intros; Elim H11; Clear H11; Intros _ H11; Cut ``a<x1``.
Intro; Unfold h; Case (total_order_Rle x a); Intro.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H4)).
Case (total_order_Rle x1 a); Intro.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H12)).
Case (total_order_Rle x b); Intro.
Case (total_order_Rle x1 b); Intro.
Rewrite H6; Elim H10; Intros; Elim r0; Intro.
Apply H14; Split.
Unfold D_x no_cond; Split.
Trivial.
Red; Intro; Rewrite <- H16 in H15; Elim (Rlt_antirefl ? H15).
Rewrite H6 in H11; Apply Rlt_le_trans with ``(Rmin x0 (b-a))``.
Apply H11.
Apply Rmin_l.
Rewrite H15; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
Rewrite H6; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
Elim n1; Right; Assumption.
Rewrite H6 in H11; Apply Ropp_Rlt; Apply Rlt_anti_compatibility with b; Apply Rle_lt_trans with ``(Rabsolu (x1-b))``.
Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply Rle_Rabsolu.
Apply Rlt_le_trans with ``(Rmin x0 (b-a))``.
Assumption.
Apply Rmin_r.
Unfold continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Exists ``x-b``; Split.
Change ``0<x-b``; Apply Rlt_Rminus; Assumption.
Intros; Elim H8; Clear H8; Intros.
Assert H10 : ``b<x0``.
Apply Ropp_Rlt; Apply Rlt_anti_compatibility with x; Apply Rle_lt_trans with ``(Rabsolu (x0-x))``.
Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply Rle_Rabsolu.
Assumption.
Unfold h; Case (total_order_Rle x a); Intro.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H4)).
Case (total_order_Rle x b); Intro.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H6)).
Case (total_order_Rle x0 a); Intro.
Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H1 (Rlt_le_trans ? ? ? H10 r))).
Case (total_order_Rle x0 b); Intro.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H10)).
Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
Intros; Elim H3; Intros; Unfold h; Case (total_order_Rle c a); Intro.
Elim r; Intro.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H4 H6)).
Rewrite H6; Reflexivity.
Case (total_order_Rle c b); Intro.
Reflexivity.
Elim n0; Assumption.
Exists [_:R](f0 a); Split.
Apply derivable_continuous; Apply (derivable_const (f0 a)).
Intros; Elim H2; Intros; Rewrite H1 in H3; Cut b==c.
Intro; Rewrite <- H5; Rewrite H1; Reflexivity.
Apply Rle_antisym; Assumption.
Qed.

(**********)
Lemma continuity_ab_maj : (f:R->R;a,b:R) ``a<=b`` -> ((c:R)``a<=c<=b``->(continuity_pt f c)) -> (EXT Mx : R |  ((c:R)``a<=c<=b``->``(f c)<=(f Mx)``)/\``a<=Mx<=b``).
Intros; Cut (EXT g:R->R | (continuity g)/\((c:R)``a<=c<=b``->(g c)==(f0 c))).
Intro HypProl.
Elim HypProl; Intros g Hcont_eq.
Elim Hcont_eq; Clear Hcont_eq; Intros Hcont Heq.
Assert H1 := (compact_P3 a b).
Assert H2 := (continuity_compact g [c:R]``a<=c<=b`` Hcont H1).
Assert H3 := (compact_P2 ? H2).
Assert H4 := (compact_P1 ? H2).
Cut (bound (image_dir g [c:R]``a <= c <= b``)).
Cut (ExT [x:R] ((image_dir g [c:R]``a <= c <= b``) x)).
Intros; Assert H7 := (complet ? H6 H5).
Elim H7; Clear H7; Intros M H7; Cut (image_dir g [c:R]``a <= c <= b`` M).
Intro; Unfold image_dir in H8; Elim H8; Clear H8; Intros Mxx H8; Elim H8; Clear H8; Intros; Exists Mxx; Split.
Intros; Rewrite <- (Heq c H10); Rewrite <- (Heq Mxx H9); Intros; Rewrite <- H8; Unfold is_lub in H7; Elim H7; Clear H7; Intros H7 _; Unfold is_upper_bound in H7; Apply H7; Unfold image_dir; Exists c; Split; [Reflexivity | Apply H10].
Apply H9.
Elim (classic (image_dir g [c:R]``a <= c <= b`` M)); Intro.
Assumption.
Cut (EXT eps:posreal | (y:R)~(intersection_domain (disc M eps) (image_dir g [c:R]``a <= c <= b``) y)).
Intro; Elim H9; Clear H9; Intros eps H9; Unfold is_lub in H7; Elim H7; Clear H7; Intros; Cut (is_upper_bound (image_dir g [c:R]``a <= c <= b``) ``M-eps``).
Intro; Assert H12 := (H10 ? H11); Cut ``M-eps<M``.
Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H12 H13)).
Pattern 2 M; Rewrite <- Rplus_Or; Unfold Rminus; Apply Rlt_compatibility; Apply Ropp_Rlt; Rewrite Ropp_O; Rewrite Ropp_Ropp; Apply (cond_pos eps).
Unfold is_upper_bound image_dir; Intros; Cut ``x<=M``.
Intro; Case (total_order_Rle x ``M-eps``); Intro.
Apply r.
Elim (H9 x); Unfold intersection_domain disc image_dir; Split.
Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Rewrite Rabsolu_right.
Apply Rlt_anti_compatibility with ``x-eps``; Replace ``x-eps+(M-x)`` with ``M-eps``.
Replace ``x-eps+eps`` with x.
Auto with real.
Ring.
Ring.
Apply Rge_minus; Apply Rle_sym1; Apply H12.
Apply H11.
Apply H7; Apply H11.
Cut (EXT V:R->Prop | (neighbourhood V M)/\((y:R)~(intersection_domain V (image_dir g [c:R]``a <= c <= b``) y))).
Intro; Elim H9; Intros V H10; Elim H10; Clear H10; Intros.
Unfold neighbourhood in H10; Elim H10; Intros del H12; Exists del; Intros; Red; Intro; Elim (H11 y).
Unfold intersection_domain; Unfold intersection_domain in H13; Elim H13; Clear H13; Intros; Split.
Apply (H12 ? H13).
Apply H14.
Cut ~(point_adherent (image_dir g [c:R]``a <= c <= b``) M).
Intro; Unfold point_adherent in H9.
Assert H10 := (not_all_ex_not ? [V:R->Prop](neighbourhood V M)
            ->(EXT y:R |
                   (intersection_domain V
                     (image_dir g [c:R]``a <= c <= b``) y)) H9).
Elim H10; Intros V0 H11; Exists V0; Assert H12 := (imply_to_and ? ? H11); Elim H12; Clear H12; Intros.
Split.
Apply H12.
Apply (not_ex_all_not ? ? H13).
Red; Intro; Cut (adherence (image_dir g [c:R]``a <= c <= b``) M).
Intro; Elim (closed_set_P1 (image_dir g [c:R]``a <= c <= b``)); Intros H11 _; Assert H12 := (H11 H3).
Elim H8.
Unfold eq_Dom in H12; Elim H12; Clear H12; Intros.
Apply (H13 ? H10).
Apply H9.
Exists (g a); Unfold image_dir; Exists a; Split.
Reflexivity.
Split; [Right; Reflexivity | Apply H].
Unfold bound; Unfold bounded in H4; Elim H4; Clear H4; Intros m H4; Elim H4; Clear H4; Intros M H4; Exists M; Unfold is_upper_bound; Intros; Elim (H4 ? H5); Intros _ H6; Apply H6.
Apply prolongement_C0; Assumption.
Qed.

(**********)
Lemma continuity_ab_min : (f:(R->R); a,b:R) ``a <= b``->((c:R)``a<=c<=b``->(continuity_pt f c))->(EXT mx:R | ((c:R)``a <= c <= b``->``(f mx) <= (f c)``)/\``a <= mx <= b``).
Intros.
Cut ((c:R)``a<=c<=b``->(continuity_pt (opp_fct f0) c)).
Intro; Assert H2 := (continuity_ab_maj (opp_fct f0) a b H H1); Elim H2; Intros x0 H3; Exists x0; Intros; Split.
Intros; Rewrite <- (Ropp_Ropp (f0 x0)); Rewrite <- (Ropp_Ropp (f0 c)); Apply Rle_Ropp1; Elim H3; Intros; Unfold opp_fct in H5; Apply H5; Apply H4.
Elim H3; Intros; Assumption.
Intros.
Assert H2 := (H0 ? H1).
Apply (continuity_pt_opp ? ? H2).
Qed.


(********************************************************)
(*         Proof of Bolzano-Weierstrass theorem         *)
(********************************************************)

Definition ValAdh [un:nat->R;x:R] : Prop := (V:R->Prop;N:nat) (neighbourhood V x) -> (EX p:nat | (le N p)/\(V (un p))).

Definition intersection_family [f:family] : R->Prop := [x:R](y:R)(ind f y)->(f y x).

Lemma ValAdh_un_exists : (un:nat->R) let D=[x:R](EX n:nat | x==(INR n)) in let f=[x:R](adherence [y:R](EX p:nat | y==(un p)/\``x<=(INR p)``)/\(D x)) in ((x:R)(EXT y:R | (f x y))->(D x)).
Intros; Elim H; Intros; Unfold f in H0; Unfold adherence in H0; Unfold point_adherent in H0; Assert H1 : (neighbourhood (disc x0 (mkposreal ? Rlt_R0_R1)) x0).
Unfold neighbourhood disc; Exists (mkposreal ? Rlt_R0_R1); Unfold included; Trivial.
Elim (H0 ? H1); Intros; Unfold intersection_domain in H2; Elim H2; Intros; Elim H4; Intros; Apply H6.
Qed.

Definition ValAdh_un [un:nat->R] : R->Prop := let D=[x:R](EX n:nat | x==(INR n)) in let f=[x:R](adherence [y:R](EX p:nat | y==(un p)/\``x<=(INR p)``)/\(D x)) in (intersection_family (mkfamily D f (ValAdh_un_exists un))).

Lemma ValAdh_un_prop : (un:nat->R;x:R) (ValAdh un x) <-> (ValAdh_un un x).
Intros; Split; Intro.
Unfold ValAdh in H; Unfold ValAdh_un; Unfold intersection_family; Simpl; Intros; Elim H0; Intros N H1; Unfold adherence; Unfold point_adherent; Intros; Elim (H V N H2); Intros; Exists (un x0); Unfold intersection_domain; Elim H3; Clear H3; Intros; Split.
Assumption.
Split.
Exists x0; Split; [Reflexivity | Rewrite H1; Apply (le_INR ? ? H3)].
Exists N; Assumption.
Unfold ValAdh; Intros; Unfold ValAdh_un in H; Unfold intersection_family in H; Simpl in H; Assert H1 : (adherence [y0:R](EX p:nat | ``y0 == (un p)``/\``(INR N) <= (INR p)``)/\(EX n:nat | ``(INR N) == (INR n)``) x).
Apply H; Exists N; Reflexivity.
Unfold adherence in H1; Unfold point_adherent in H1; Assert H2 := (H1 ? H0); Elim H2; Intros; Unfold intersection_domain in H3; Elim H3; Clear H3; Intros; Elim H4; Clear H4; Intros; Elim H4; Clear H4; Intros; Elim H4; Clear H4; Intros; Exists x1; Split.
Apply (INR_le ? ? H6).
Rewrite H4 in H3; Apply H3.
Qed.

Lemma adherence_P4 : (F,G:R->Prop) (included F G) -> (included (adherence F) (adherence G)).
Unfold adherence included; Unfold point_adherent; Intros; Elim (H0 ? H1); Unfold intersection_domain; Intros; Elim H2; Clear H2; Intros; Exists x0; Split; [Assumption | Apply (H ? H3)].
Qed.

Definition family_closed_set [f:family] : Prop := (x:R) (closed_set (f x)).

Definition intersection_vide_in [D:R->Prop;f:family] : Prop := ((x:R)((ind f x)->(included (f x) D))/\~(EXT y:R | (intersection_family f y))).

Definition intersection_vide_finite_in [D:R->Prop;f:family] : Prop := (intersection_vide_in D f)/\(family_finite f).

(**********)
Lemma compact_P6 : (X:R->Prop) (compact X) -> (EXT z:R | (X z)) -> ((g:family) (family_closed_set g) -> (intersection_vide_in X g) -> (EXT D:R->Prop | (intersection_vide_finite_in X (subfamily g D)))).
Intros X H Hyp g H0 H1.
Pose D' := (ind g).
Pose f' := [x:R][y:R](complementary (g x) y)/\(D' x).
Assert H2 : (x:R)(EXT y:R|(f' x y))->(D' x).
Intros; Elim H2; Intros; Unfold f' in H3; Elim H3; Intros; Assumption.
Pose f0 := (mkfamily D' f' H2).
Unfold compact in H; Assert H3 : (covering_open_set X f0).
Unfold covering_open_set; Split.
Unfold covering; Intros; Unfold intersection_vide_in in H1; Elim (H1 x); Intros; Unfold intersection_family in H5; Assert H6 := (not_ex_all_not ? [y:R](y0:R)(ind g y0)->(g y0 y) H5 x); Assert H7 := (not_all_ex_not ? [y0:R](ind g y0)->(g y0 x) H6); Elim H7; Intros; Exists x0; Elim (imply_to_and ? ? H8); Intros; Unfold f0; Simpl; Unfold f'; Split; [Apply H10 | Apply H9].
Unfold family_open_set; Intro; Elim (classic (D' x)); Intro.
Apply open_set_P6 with (complementary (g x)).
Unfold family_closed_set in H0; Unfold closed_set in H0; Apply H0.
Unfold f0; Simpl; Unfold f'; Unfold eq_Dom; Split.
Unfold included; Intros; Split; [Apply H4 | Apply H3].
Unfold included; Intros; Elim H4; Intros; Assumption.
Apply open_set_P6 with [_:R]False.
Apply open_set_P4.
Unfold eq_Dom; Unfold included; Split; Intros; [Elim H4 | Simpl in H4; Unfold f' in H4; Elim H4; Intros; Elim H3; Assumption].
Elim (H ? H3); Intros SF H4; Exists SF; Unfold intersection_vide_finite_in; Split.
Unfold intersection_vide_in; Simpl; Intros; Split.
Intros; Unfold included; Intros; Unfold intersection_vide_in in H1; Elim (H1 x); Intros; Elim H6; Intros; Apply H7.
Unfold intersection_domain in H5; Elim H5; Intros; Assumption.
Assumption.
Elim (classic (EXT y:R | (intersection_domain (ind g) SF y))); Intro Hyp'.
Red; Intro; Elim H5; Intros; Unfold intersection_family in H6; Simpl in H6.
Cut (X x0).
Intro; Unfold covering_finite in H4; Elim H4; Clear H4; Intros H4 _; Unfold covering in H4; Elim (H4 x0 H7); Intros; Simpl in H8; Unfold intersection_domain in H6; Cut (ind g x1)/\(SF x1).
Intro; Assert H10 := (H6 x1 H9); Elim H10; Clear H10; Intros H10 _; Elim H8; Clear H8; Intros H8 _; Unfold f' in H8; Unfold complementary in H8; Elim H8; Clear H8; Intros H8 _; Elim H8; Assumption.
Split.
Apply (cond_fam f0).
Exists x0; Elim H8; Intros; Assumption.
Elim H8; Intros; Assumption.
Unfold intersection_vide_in in H1; Elim Hyp'; Intros; Assert H8 := (H6 ? H7); Elim H8; Intros; Cut (ind g x1).
Intro; Elim (H1 x1); Intros; Apply H12.
Apply H11.
Apply H9.
Apply (cond_fam g); Exists x0; Assumption.
Unfold covering_finite in H4; Elim H4; Clear H4; Intros H4 _; Cut (EXT z:R | (X z)).
Intro; Elim H5; Clear H5; Intros; Unfold covering in H4; Elim (H4 x0 H5); Intros; Simpl in H6; Elim Hyp'; Exists x1; Elim H6; Intros; Unfold intersection_domain; Split.
Apply (cond_fam f0); Exists x0; Apply H7.
Apply H8.
Apply Hyp.
Unfold covering_finite in H4; Elim H4; Clear H4; Intros; Unfold family_finite in H5; Unfold domain_finite in H5; Unfold family_finite; Unfold domain_finite; Elim H5; Clear H5; Intros l H5; Exists l; Intro; Elim (H5 x); Intros; Split; Intro; [Apply H6; Simpl; Simpl in H8; Apply H8 | Apply (H7 H8)].
Qed.

Theorem Bolzano_Weierstrass : (un:nat->R;X:R->Prop) (compact X) -> ((n:nat)(X (un n))) -> (EXT l:R | (ValAdh un l)).
Intros; Cut (EXT l:R | (ValAdh_un un l)).
Intro; Elim H1; Intros; Exists x; Elim (ValAdh_un_prop un x); Intros; Apply (H4 H2).
Assert H1 : (EXT z:R | (X z)).
Exists (un O); Apply H0.
Pose D:=[x:R](EX n:nat | x==(INR n)).
Pose g:=[x:R](adherence [y:R](EX p:nat | y==(un p)/\``x<=(INR p)``)/\(D x)).
Assert H2 : (x:R)(EXT y:R | (g x y))->(D x).
Intros; Elim H2; Intros; Unfold g in H3; Unfold adherence in H3; Unfold point_adherent in H3.
Assert H4 : (neighbourhood (disc x0 (mkposreal ? Rlt_R0_R1)) x0).
Unfold neighbourhood; Exists (mkposreal ? Rlt_R0_R1); Unfold included; Trivial.
Elim (H3 ? H4); Intros; Unfold intersection_domain in H5; Decompose [and] H5; Assumption.
Pose f0 := (mkfamily D g H2).
Assert H3 := (compact_P6 X H H1 f0).
Elim (classic (EXT l:R | (ValAdh_un un l))); Intro.
Assumption.
Cut (family_closed_set f0).
Intro; Cut (intersection_vide_in X f0).
Intro; Assert H7 := (H3 H5 H6).
Elim H7; Intros SF H8; Unfold intersection_vide_finite_in in H8; Elim H8; Clear H8; Intros; Unfold intersection_vide_in in H8; Elim (H8 R0); Intros _ H10; Elim H10; Unfold family_finite in H9; Unfold domain_finite in H9; Elim H9; Clear H9; Intros l H9; Pose r := (MaxRlist l); Cut (D r).
Intro; Unfold D in H11; Elim H11; Intros; Exists (un x); Unfold intersection_family; Simpl; Unfold intersection_domain; Intros; Split.
Unfold g; Apply adherence_P1; Split.
Exists x; Split; [Reflexivity | Rewrite <- H12; Unfold r; Apply MaxRlist_P1; Elim (H9 y); Intros; Apply H14; Simpl; Apply H13].
Elim H13; Intros; Assumption.
Elim H13; Intros; Assumption.
Elim (H9 r); Intros.
Simpl in H12; Unfold intersection_domain in H12; Cut (In r l).
Intro; Elim (H12 H13); Intros; Assumption.
Unfold r; Apply MaxRlist_P2; Cut (EXT z:R | (intersection_domain (ind f0) SF z)).
Intro; Elim H13; Intros; Elim (H9 x); Intros; Simpl in H15; Assert H17 := (H15 H14); Exists x; Apply H17.
Elim (classic (EXT z:R | (intersection_domain (ind f0) SF z))); Intro.
Assumption.
Elim (H8 R0); Intros _ H14; Elim H1; Intros; Assert H16 := (not_ex_all_not ? [y:R](intersection_family (subfamily f0 SF) y) H14); Assert H17 := (not_ex_all_not ? [z:R](intersection_domain (ind f0) SF z) H13); Assert H18 := (H16 x); Unfold intersection_family in H18; Simpl in H18; Assert H19 := (not_all_ex_not ? [y:R](intersection_domain D SF y)->(g y x)/\(SF y) H18); Elim H19; Intros; Assert H21 := (imply_to_and ? ? H20); Elim (H17 x0); Elim H21; Intros; Assumption.
Unfold intersection_vide_in; Intros; Split.
Intro; Simpl in H6; Unfold f0; Simpl; Unfold g; Apply included_trans with (adherence X).
Apply adherence_P4.
Unfold included; Intros; Elim H7; Intros; Elim H8; Intros; Elim H10; Intros; Rewrite H11; Apply H0.
Apply adherence_P2; Apply compact_P2; Assumption.
Apply H4.
Unfold family_closed_set; Unfold f0; Simpl; Unfold g; Intro; Apply adherence_P3.
Qed.

(********************************************************)
(*               Proof of Heine's theorem               *)
(********************************************************)

Definition uniform_continuity [f:R->R;X:R->Prop] : Prop := (eps:posreal)(EXT delta:posreal | (x,y:R) (X x)->(X y)->``(Rabsolu (x-y))<delta`` ->``(Rabsolu ((f x)-(f y)))<eps``).

Lemma is_lub_u : (E:R->Prop;x,y:R) (is_lub E x) -> (is_lub E y) -> x==y.
Unfold is_lub; Intros; Elim H; Elim H0; Intros; Apply Rle_antisym; [Apply (H4 ? H1) | Apply (H2 ? H3)].
Qed.

Lemma domain_P1 : (X:R->Prop) ~(EXT y:R | (X y))\/(EXT y:R | (X y)/\((x:R)(X x)->x==y))\/(EXT x:R | (EXT y:R | (X x)/\(X y)/\``x<>y``)).
Intro; Elim (classic (EXT y:R | (X y))); Intro.
Right; Elim H; Intros; Elim (classic (EXT y:R | (X y)/\``y<>x``)); Intro.
Right; Elim H1; Intros; Elim H2; Intros; Exists x; Exists x0; Intros.
Split; [Assumption | Split; [Assumption | Apply not_sym; Assumption]].
Left; Exists x; Split.
Assumption.
Intros; Case (Req_EM x0 x); Intro.
Assumption.
Elim H1; Exists x0; Split; Assumption.
Left; Assumption.
Qed.

Theorem Heine : (f:R->R;X:R->Prop) (compact X) -> ((x:R)(X x)->(continuity_pt f x)) -> (uniform_continuity f X).
Intros f0 X H0 H; Elim (domain_P1 X); Intro Hyp.
(* X est vide *)
Unfold uniform_continuity; Intros; Exists (mkposreal ? Rlt_R0_R1); Intros; Elim Hyp; Exists x; Assumption.
Elim Hyp; Clear Hyp; Intro Hyp.
(* X possde un seul lment *)
Unfold uniform_continuity; Intros; Exists (mkposreal ? Rlt_R0_R1); Intros; Elim Hyp; Clear Hyp; Intros; Elim H4; Clear H4; Intros; Assert H6 := (H5 ? H1); Assert H7 := (H5 ? H2); Rewrite H6; Rewrite H7; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply (cond_pos eps).
(* X possde au moins deux lments distincts *)
Assert X_enc : (EXT m:R | (EXT M:R | ((x:R)(X x)->``m<=x<=M``)/\``m<M``)).
Assert H1 := (compact_P1 X H0); Unfold bounded in H1; Elim H1; Intros; Elim H2; Intros; Exists x; Exists x0; Split.
Apply H3.
Elim Hyp; Intros; Elim H4; Intros; Decompose [and] H5; Assert H10 := (H3 ? H6); Assert H11 := (H3 ? H8); Elim H10; Intros; Elim H11; Intros; Case (total_order_T x x0); Intro.
Elim s; Intro.
Assumption.
Rewrite b in H13; Rewrite b in H7; Elim H9; Apply Rle_antisym; Apply Rle_trans with x0; Assumption.
Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? (Rle_trans ? ? ? H13 H14) r)).
Elim X_enc; Clear X_enc; Intros m X_enc; Elim X_enc; Clear X_enc; Intros M X_enc; Elim X_enc; Clear X_enc Hyp; Intros X_enc Hyp; Unfold uniform_continuity; Intro; Assert H1 : (t:posreal)``0<t/2``.
Intro; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos t) | Apply Rlt_Rinv; Sup0].
Pose g := [x:R][y:R](X x)/\(EXT del:posreal | ((z:R) ``(Rabsolu (z-x))<del``->``(Rabsolu ((f0 z)-(f0 x)))<eps/2``)/\(is_lub [zeta:R]``0<zeta<=M-m``/\((z:R) ``(Rabsolu (z-x))<zeta``->``(Rabsolu ((f0 z)-(f0 x)))<eps/2``) del)/\(disc x (mkposreal ``del/2`` (H1 del)) y)).
Assert H2 : (x:R)(EXT y:R | (g x y))->(X x).
Intros; Elim H2; Intros; Unfold g in H3; Elim H3; Clear H3; Intros H3 _; Apply H3.
Pose f' := (mkfamily X g H2); Unfold compact in H0; Assert H3 : (covering_open_set X f').
Unfold covering_open_set; Split.
Unfold covering; Intros; Exists x; Simpl; Unfold g; Split.
Assumption.
Assert H4 := (H ? H3); Unfold continuity_pt in H4; Unfold continue_in in H4; Unfold limit1_in in H4; Unfold limit_in in H4; Simpl in H4; Unfold R_dist in H4; Elim (H4 ``eps/2`` (H1 eps)); Intros; Pose E:=[zeta:R]``0<zeta <= M-m``/\((z:R)``(Rabsolu (z-x)) < zeta``->``(Rabsolu ((f0 z)-(f0 x))) < eps/2``); Assert H6 : (bound E).
Unfold bound; Exists ``M-m``; Unfold is_upper_bound; Unfold E; Intros; Elim H6; Clear H6; Intros H6 _; Elim H6; Clear H6; Intros _ H6; Apply H6.
Assert H7 : (EXT x:R | (E x)).
Elim H5; Clear H5; Intros; Exists (Rmin x0 ``M-m``); Unfold E; Intros; Split.
Split.
Unfold Rmin; Case (total_order_Rle x0 ``M-m``); Intro.
Apply H5.
Apply Rlt_Rminus; Apply Hyp.
Apply Rmin_r.
Intros; Case (Req_EM x z); Intro.
Rewrite H9; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply (H1 eps).
Apply H7; Split.
Unfold D_x no_cond; Split; [Trivial | Assumption].
Apply Rlt_le_trans with (Rmin x0 ``M-m``); [Apply H8 | Apply Rmin_l].
Assert H8 := (complet ? H6 H7); Elim H8; Clear H8; Intros; Cut ``0<x1<=(M-m)``.
Intro; Elim H8; Clear H8; Intros; Exists (mkposreal ? H8); Split.
Intros; Cut (EXT alp:R | ``(Rabsolu (z-x))<alp<=x1``/\(E alp)).
Intros; Elim H11; Intros; Elim H12; Clear H12; Intros; Unfold E in H13; Elim H13; Intros; Apply H15.
Elim H12; Intros; Assumption.
Elim (classic (EXT alp:R | ``(Rabsolu (z-x)) < alp <= x1``/\(E alp))); Intro.
Assumption.
Assert H12 := (not_ex_all_not ? [alp:R]``(Rabsolu (z-x)) < alp <= x1``/\(E alp) H11); Unfold is_lub in p; Elim p; Intros; Cut (is_upper_bound E ``(Rabsolu (z-x))``).
Intro; Assert H16 := (H14 ? H15); Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H10 H16)).
Unfold is_upper_bound; Intros; Unfold is_upper_bound in H13; Assert H16 := (H13 ? H15); Case (total_order_Rle x2 ``(Rabsolu (z-x))``); Intro.
Assumption.
Elim (H12 x2); Split; [Split; [Auto with real | Assumption] | Assumption].
Split.
Apply p.
Unfold disc; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Simpl; Unfold Rdiv; Apply Rmult_lt_pos; [Apply H8 | Apply Rlt_Rinv; Sup0].
Elim H7; Intros; Unfold E in H8; Elim H8; Intros H9 _; Elim H9; Intros H10 _; Unfold is_lub in p; Elim p; Intros; Unfold is_upper_bound in H12; Unfold is_upper_bound in H11; Split.
Apply Rlt_le_trans with x2; [Assumption | Apply (H11 ? H8)].
Apply H12; Intros; Unfold E in H13; Elim H13; Intros; Elim H14; Intros; Assumption.
Unfold family_open_set; Intro; Simpl; Elim (classic (X x)); Intro.
Unfold g; Unfold open_set; Intros; Elim H4; Clear H4; Intros _ H4; Elim H4; Clear H4; Intros; Elim H4; Clear H4; Intros; Unfold neighbourhood; Case (Req_EM x x0); Intro.
Exists (mkposreal ? (H1 x1)); Rewrite <- H6; Unfold included; Intros; Split.
Assumption.
Exists x1; Split.
Apply H4.
Split.
Elim H5; Intros; Apply H8.
Apply H7.
Pose d := ``x1/2-(Rabsolu (x0-x))``; Assert H7 : ``0<d``.
Unfold d; Apply Rlt_Rminus; Elim H5; Clear H5; Intros; Unfold disc in H7; Apply H7.
Exists (mkposreal ? H7); Unfold included; Intros; Split.
Assumption.
Exists x1; Split.
Apply H4.
Elim H5; Intros; Split.
Assumption.
Unfold disc in H8; Simpl in H8; Unfold disc; Simpl; Unfold disc in H10; Simpl in H10; Apply Rle_lt_trans with ``(Rabsolu (x2-x0))+(Rabsolu (x0-x))``.
Replace ``x2-x`` with ``(x2-x0)+(x0-x)``; [Apply Rabsolu_triang | Ring].
Replace ``x1/2`` with ``d+(Rabsolu (x0-x))``; [Idtac | Unfold d; Ring].
Do 2 Rewrite <- (Rplus_sym ``(Rabsolu (x0-x))``); Apply Rlt_compatibility; Apply H8.
Apply open_set_P6 with [_:R]False.
Apply open_set_P4.
Unfold eq_Dom; Unfold included; Intros; Split.
Intros; Elim H4.
Intros; Unfold g in H4; Elim H4; Clear H4; Intros H4 _; Elim H3; Apply H4.
Elim (H0 ? H3); Intros DF H4; Unfold covering_finite in H4; Elim H4; Clear H4; Intros; Unfold family_finite in H5; Unfold domain_finite in H5; Unfold covering in H4; Simpl in H4; Simpl in H5; Elim H5; Clear H5; Intros l H5; Unfold intersection_domain in H5; Cut (x:R)(In x l)->(EXT del:R | ``0<del``/\((z:R)``(Rabsolu (z-x)) < del``->``(Rabsolu ((f0 z)-(f0 x))) < eps/2``)/\(included (g x) [z:R]``(Rabsolu (z-x))<del/2``)).
Intros; Assert H7 := (Rlist_P1 l [x:R][del:R]``0<del``/\((z:R)``(Rabsolu (z-x)) < del``->``(Rabsolu ((f0 z)-(f0 x))) < eps/2``)/\(included (g x) [z:R]``(Rabsolu (z-x))<del/2``) H6); Elim H7; Clear H7; Intros l' H7; Elim H7; Clear H7; Intros; Pose D := (MinRlist l'); Cut ``0<D/2``.
Intro; Exists (mkposreal ? H9); Intros; Assert H13 := (H4 ? H10); Elim H13; Clear H13; Intros xi H13; Assert H14 : (In xi l).
Unfold g in H13; Decompose [and] H13; Elim (H5 xi); Intros; Apply H14; Split; Assumption.
Elim (pos_Rl_P2 l xi); Intros H15 _; Elim (H15 H14); Intros i H16; Elim H16; Intros; Apply Rle_lt_trans with ``(Rabsolu ((f0 x)-(f0 xi)))+(Rabsolu ((f0 xi)-(f0 y)))``.
Replace ``(f0 x)-(f0 y)`` with ``((f0 x)-(f0 xi))+((f0 xi)-(f0 y))``; [Apply Rabsolu_triang | Ring].
Rewrite (double_var eps); Apply Rplus_lt.
Assert H19 := (H8 i H17); Elim H19; Clear H19; Intros; Rewrite <- H18 in H20; Elim H20; Clear H20; Intros; Apply H20; Unfold included in H21; Apply Rlt_trans with ``(pos_Rl l' i)/2``.
Apply H21.
Elim H13; Clear H13; Intros; Assumption.
Unfold Rdiv; Apply Rlt_monotony_contra with ``2``.
Sup0.
Rewrite Rmult_sym; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
Rewrite Rmult_1r; Pattern 1 (pos_Rl l' i); Rewrite <- Rplus_Or; Rewrite double; Apply Rlt_compatibility; Apply H19.
DiscrR.
Assert H19 := (H8 i H17); Elim H19; Clear H19; Intros; Rewrite <- H18 in H20; Elim H20; Clear H20; Intros; Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H20; Unfold included in H21; Elim H13; Intros; Assert H24 := (H21 x H22); Apply Rle_lt_trans with ``(Rabsolu (y-x))+(Rabsolu (x-xi))``.
Replace ``y-xi`` with ``(y-x)+(x-xi)``; [Apply Rabsolu_triang | Ring].
Rewrite (double_var (pos_Rl l' i)); Apply Rplus_lt.
Apply Rlt_le_trans with ``D/2``.
Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H12.
Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/2``); Apply Rle_monotony.
Left; Apply Rlt_Rinv; Sup0.
Unfold D; Apply MinRlist_P1; Elim (pos_Rl_P2 l' (pos_Rl l' i)); Intros; Apply H26; Exists i; Split; [Rewrite <- H7; Assumption | Reflexivity].
Assumption.
Unfold Rdiv; Apply Rmult_lt_pos; [Unfold D; Apply MinRlist_P2; Intros; Elim (pos_Rl_P2 l' y); Intros; Elim (H10 H9); Intros; Elim H12; Intros; Rewrite H14; Rewrite <- H7 in H13; Elim (H8 x H13); Intros; Apply H15 | Apply Rlt_Rinv; Sup0].
Intros; Elim (H5 x); Intros; Elim (H8 H6); Intros; Pose E:=[zeta:R]``0<zeta <= M-m``/\((z:R)``(Rabsolu (z-x)) < zeta``->``(Rabsolu ((f0 z)-(f0 x))) < eps/2``); Assert H11 : (bound E).
Unfold bound; Exists ``M-m``; Unfold is_upper_bound; Unfold E; Intros; Elim H11; Clear H11; Intros H11 _; Elim H11; Clear H11; Intros _ H11; Apply H11.
Assert H12 : (EXT x:R | (E x)).
Assert H13 := (H ? H9); Unfold continuity_pt in H13; Unfold continue_in in H13; Unfold limit1_in in H13; Unfold limit_in in H13; Simpl in H13; Unfold R_dist in H13; Elim (H13 ? (H1 eps)); Intros; Elim H12; Clear H12; Intros; Exists (Rmin x0 ``M-m``); Unfold E; Intros; Split.
Split; [Unfold Rmin; Case (total_order_Rle x0 ``M-m``); Intro; [Apply H12 | Apply Rlt_Rminus; Apply Hyp] | Apply Rmin_r].
Intros; Case (Req_EM x z); Intro.
Rewrite H16; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply (H1 eps).
Apply H14; Split; [Unfold D_x no_cond; Split; [Trivial | Assumption] | Apply Rlt_le_trans with (Rmin x0 ``M-m``); [Apply H15 | Apply Rmin_l]].
Assert H13 := (complet ? H11 H12); Elim H13; Clear H13; Intros; Cut ``0<x0<=M-m``.
Intro; Elim H13; Clear H13; Intros; Exists x0; Split.
Assumption.
Split.
Intros; Cut (EXT alp:R | ``(Rabsolu (z-x))<alp<=x0``/\(E alp)).
Intros; Elim H16; Intros; Elim H17; Clear H17; Intros; Unfold E in H18; Elim H18; Intros; Apply H20; Elim H17; Intros; Assumption.
Elim (classic (EXT alp:R | ``(Rabsolu (z-x)) < alp <= x0``/\(E alp))); Intro.
Assumption.
Assert H17 := (not_ex_all_not ? [alp:R]``(Rabsolu (z-x)) < alp <= x0``/\(E alp) H16); Unfold is_lub in p; Elim p; Intros; Cut (is_upper_bound E ``(Rabsolu (z-x))``).
Intro; Assert H21 := (H19 ? H20); Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H15 H21)).
Unfold is_upper_bound; Intros; Unfold is_upper_bound in H18; Assert H21 := (H18 ? H20); Case (total_order_Rle x1 ``(Rabsolu (z-x))``); Intro.
Assumption.
Elim (H17 x1); Split.
Split; [Auto with real | Assumption].
Assumption.
Unfold included g; Intros; Elim H15; Intros; Elim H17; Intros; Decompose [and] H18; Cut x0==x2.
Intro; Rewrite H20; Apply H22.
Unfold E in p; EApply is_lub_u.
Apply p.
Apply H21.
Elim H12; Intros; Unfold E in H13; Elim H13; Intros H14 _; Elim H14; Intros H15 _; Unfold is_lub in p; Elim p; Intros; Unfold is_upper_bound in H16; Unfold is_upper_bound in H17; Split.
Apply Rlt_le_trans with x1; [Assumption | Apply (H16 ? H13)].
Apply H17; Intros; Unfold E in H18; Elim H18; Intros; Elim H19; Intros; Assumption.
Qed.