path: root/theories/Reals/Rtopology.v

(************************************************************************)
(*  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 10710 2008-03-23 09:24:09Z herbelin $ i*)

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

(** * General definitions and propositions *)

Definition included (D1 D2:R -> Prop) : Prop := forall x:R, D1 x -> D2 x.
Definition disc (x:R) (delta:posreal) (y:R) : Prop := Rabs (y - x) < delta.
Definition neighbourhood (V:R -> Prop) (x:R) : Prop :=
  exists delta : posreal, included (disc x delta) V.
Definition open_set (D:R -> Prop) : Prop :=
  forall x:R, D x -> neighbourhood D x.
Definition complementary (D:R -> Prop) (c:R) : Prop := ~ D c.
Definition closed_set (D:R -> Prop) : Prop := open_set (complementary D).
Definition intersection_domain (D1 D2:R -> Prop) (c:R) : Prop := D1 c /\ D2 c.
Definition union_domain (D1 D2:R -> Prop) (c:R) : Prop := D1 c \/ D2 c.
Definition interior (D:R -> Prop) (x:R) : Prop := neighbourhood D x.

Lemma interior_P1 : forall D:R -> Prop, included (interior D) D.
Proof.
  intros; unfold included in |- *; unfold interior in |- *; intros;
    unfold neighbourhood in H; elim H; intros; unfold included in H0; 
      apply H0; unfold disc in |- *; unfold Rminus in |- *; 
        rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos x0).
Qed.

Lemma interior_P2 : forall D:R -> Prop, open_set D -> included D (interior D).
Proof.
  intros; unfold open_set in H; unfold included in |- *; intros;
    assert (H1 := H _ H0); unfold interior in |- *; apply H1.
Qed.

Definition point_adherent (D:R -> Prop) (x:R) : Prop :=
  forall V:R -> Prop,
    neighbourhood V x ->  exists y : R, intersection_domain V D y.
Definition adherence (D:R -> Prop) (x:R) : Prop := point_adherent D x.

Lemma adherence_P1 : forall D:R -> Prop, included D (adherence D).
Proof.
  intro; unfold included in |- *; intros; unfold adherence in |- *;
    unfold point_adherent in |- *; intros; exists x;
      unfold intersection_domain in |- *; split.
  unfold neighbourhood in H0; elim H0; intros; unfold included in H1; apply H1;
    unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r;
      rewrite Rabs_R0; apply (cond_pos x0).
  apply H.
Qed.

Lemma included_trans :
  forall D1 D2 D3:R -> Prop,
    included D1 D2 -> included D2 D3 -> included D1 D3.
Proof.
  unfold included in |- *; intros; apply H0; apply H; apply H1.
Qed.

Lemma interior_P3 : forall D:R -> Prop, open_set (interior D).
Proof.
  intro; unfold open_set, interior in |- *; unfold neighbourhood in |- *;
    intros; elim H; intros.
  exists x0; unfold included in |- *; intros.
  set (del := x0 - Rabs (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 in |- *; unfold disc in |- *; intros.
  apply Rle_lt_trans with (Rabs (x3 - x1) + Rabs (x1 - x)).
  replace (x3 - x) with (x3 - x1 + (x1 - x)); [ apply Rabs_triang | ring ].
  replace (pos x0) with (del + Rabs (x1 - x)).
  do 2 rewrite <- (Rplus_comm (Rabs (x1 - x))); apply Rplus_lt_compat_l;
    apply H4.
  unfold del in |- *; rewrite <- (Rabs_Ropp (x - x1)); rewrite Ropp_minus_distr;
    ring.
  unfold del in |- *; apply Rplus_lt_reg_r with (Rabs (x - x1));
    rewrite Rplus_0_r;
      replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0);
      [ idtac | ring ].
  unfold disc in H1; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1.
Qed.

Lemma complementary_P1 :
  forall D:R -> Prop,
    ~ (exists y : R, intersection_domain D (complementary D) y).
Proof.
  intro; red in |- *; intro; elim H; intros;
    unfold intersection_domain, complementary in H0; elim H0; 
      intros; elim H2; assumption.
Qed.

Lemma adherence_P2 :
  forall D:R -> Prop, closed_set D -> included (adherence D) D.
Proof.
  unfold closed_set in |- *; unfold open_set, complementary in |- *; intros;
    unfold included, adherence in |- *; 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 : forall D:R -> Prop, closed_set (adherence D).
Proof.
  intro; unfold closed_set, adherence in |- *;
    unfold open_set, complementary, point_adherent in |- *; 
      intros;
        set
          (P :=
            fun V:R -> Prop =>
              neighbourhood V x ->  exists 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 in |- *; elim H2; intros; unfold neighbourhood in H3;
                elim H3; intros; exists x0; unfold included in |- *; 
                  intros; red in |- *; intro.
  assert (H8 := H7 V0);
    cut (exists delta : posreal, (forall x:R, disc x1 delta x -> V0 x)).
  intro; assert (H10 := H8 H9); elim H4; assumption.
  cut (0 < x0 - Rabs (x - x1)).
  intro; set (del := mkposreal _ H9); exists del; intros;
    unfold included in H5; apply H5; unfold disc in |- *;
      apply Rle_lt_trans with (Rabs (x2 - x1) + Rabs (x1 - x)).
  replace (x2 - x) with (x2 - x1 + (x1 - x)); [ apply Rabs_triang | ring ].
  replace (pos x0) with (del + Rabs (x1 - x)).
  do 2 rewrite <- (Rplus_comm (Rabs (x1 - x))); apply Rplus_lt_compat_l;
    apply H10.
  unfold del in |- *; simpl in |- *; rewrite <- (Rabs_Ropp (x - x1));
    rewrite Ropp_minus_distr; ring.
  apply Rplus_lt_reg_r with (Rabs (x - x1)); rewrite Rplus_0_r;
    replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0);
    [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H6 | ring ].
Qed.

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

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

Lemma open_set_P1 : forall D:R -> Prop, open_set D <-> D =_D interior D.
Proof.
  intro; split.
  intro; unfold eq_Dom in |- *; split.
  apply interior_P2; assumption.
  apply interior_P1.
  intro; unfold eq_Dom in H; elim H; clear H; intros; unfold open_set in |- *;
    intros; unfold included, interior in H; unfold included in H0;
      apply (H _ H1).
Qed.

Lemma closed_set_P1 : forall D:R -> Prop, closed_set D <-> D =_D adherence D.
Proof.
  intro; split.
  intro; unfold eq_Dom in |- *; split.
  apply adherence_P1.
  apply adherence_P2; assumption.
  unfold eq_Dom in |- *; unfold included in |- *; intros;
    assert (H0 := adherence_P3 D); unfold closed_set in H0;
      unfold closed_set in |- *; unfold open_set in |- *; 
        unfold open_set in H0; intros; assert (H2 : complementary (adherence D) x).
  unfold complementary in |- *; unfold complementary in H1; red in |- *; intro;
    elim H; clear H; intros _ H; elim H1; apply (H _ H2).
  assert (H3 := H0 _ H2); unfold neighbourhood in |- *;
    unfold neighbourhood in H3; elim H3; intros; exists x0;
      unfold included in |- *; unfold included in H4; intros;
        assert (H6 := H4 _ H5); unfold complementary in H6;
          unfold complementary in |- *; red in |- *; intro; 
            elim H; clear H; intros H _; elim H6; apply (H _ H7).
Qed.

Lemma neighbourhood_P1 :
  forall (D1 D2:R -> Prop) (x:R),
    included D1 D2 -> neighbourhood D1 x -> neighbourhood D2 x.
Proof.
  unfold included, neighbourhood in |- *; intros; elim H0; intros; exists x0;
    intros; unfold included in |- *; unfold included in H1; 
      intros; apply (H _ (H1 _ H2)).
Qed.

Lemma open_set_P2 :
  forall D1 D2:R -> Prop,
    open_set D1 -> open_set D2 -> open_set (union_domain D1 D2).
Proof.
  unfold open_set in |- *; intros; unfold union_domain in H1; elim H1; intro.
  apply neighbourhood_P1 with D1.
  unfold included, union_domain in |- *; tauto.
  apply H; assumption.
  apply neighbourhood_P1 with D2.
  unfold included, union_domain in |- *; tauto.
  apply H0; assumption.
Qed.

Lemma open_set_P3 :
  forall D1 D2:R -> Prop,
    open_set D1 -> open_set D2 -> open_set (intersection_domain D1 D2).
Proof.
  unfold open_set in |- *; intros; unfold intersection_domain in H1; elim H1;
    intros.
  assert (H4 := H _ H2); assert (H5 := H0 _ H3);
    unfold intersection_domain in |- *; 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; set (del := mkposreal _ H6).
  exists del; unfold included in |- *; 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 in |- *; simpl in |- *; apply Rmin_l.
  apply H0; apply Rlt_le_trans with (pos del).
  apply H7.
  unfold del in |- *; simpl in |- *; apply Rmin_r.
  unfold Rmin in |- *; case (Rle_dec del1 del2); intro.
  apply (cond_pos del1).
  apply (cond_pos del2).
Qed.

Lemma open_set_P4 : open_set (fun x:R => False).
Proof.
  unfold open_set in |- *; intros; elim H.
Qed.

Lemma open_set_P5 : open_set (fun x:R => True).
Proof.
  unfold open_set in |- *; intros; unfold neighbourhood in |- *.
  exists (mkposreal 1 Rlt_0_1); unfold included in |- *; intros; trivial.
Qed.

Lemma disc_P1 : forall (x:R) (del:posreal), open_set (disc x del).
Proof.
  intros; assert (H := open_set_P1 (disc x del)).
  elim H; intros; apply H1.
  unfold eq_Dom in |- *; split.
  unfold included, interior, disc in |- *; intros;
    cut (0 < del - Rabs (x - x0)).
  intro; set (del2 := mkposreal _ H3).
  exists del2; unfold included in |- *; intros.
  apply Rle_lt_trans with (Rabs (x1 - x0) + Rabs (x0 - x)).
  replace (x1 - x) with (x1 - x0 + (x0 - x)); [ apply Rabs_triang | ring ].
  replace (pos del) with (del2 + Rabs (x0 - x)).
  do 2 rewrite <- (Rplus_comm (Rabs (x0 - x))); apply Rplus_lt_compat_l.
  apply H4.
  unfold del2 in |- *; simpl in |- *; rewrite <- (Rabs_Ropp (x - x0));
    rewrite Ropp_minus_distr; ring.
  apply Rplus_lt_reg_r with (Rabs (x - x0)); rewrite Rplus_0_r;
    replace (Rabs (x - x0) + (del - Rabs (x - x0))) with (pos del);
    [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2 | ring ].
  apply interior_P1.
Qed.

Lemma continuity_P1 :
  forall (f:R -> R) (x:R),
    continuity_pt f x <->
    (forall W:R -> Prop,
      neighbourhood W (f x) ->
      exists V : R -> Prop,
        neighbourhood V x /\ (forall y:R, V y -> W (f y))).
Proof.
  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 in |- *.
  exists (mkposreal del2 H4).
  unfold included in |- *; intros; assumption.
  intros; apply H1; unfold disc in |- *; case (Req_dec y x); intro.
  rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
    apply (cond_pos del1).
  apply H5; split.
  unfold D_x, no_cond in |- *; split.
  trivial.
  apply (sym_not_eq (A:=R)); apply H7.
  unfold disc in H6; apply H6.
  intros; unfold continuity_pt in |- *; unfold continue_in in |- *;
    unfold limit1_in in |- *; unfold limit_in 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 in |- *;
    unfold R_dist in |- *; apply (H6 _ (H7 _ H10)).
  unfold neighbourhood, disc in |- *; exists (mkposreal eps H0);
    unfold included in |- *; intros; assumption.
Qed.

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

(**********)
Lemma continuity_P2 :
  forall (f:R -> R) (D:R -> Prop),
    continuity f -> open_set D -> open_set (image_rec f D).
Proof.
  intros; unfold open_set in H0; unfold open_set in |- *; intros;
    assert (H2 := continuity_P1 f x); elim H2; intros H3 _;
      assert (H4 := H3 (H x)); unfold neighbourhood, image_rec in |- *;
        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 in |- *; intros; apply (H8 _ (H9 _ H10)).
Qed.

(**********)
Lemma continuity_P3 :
  forall f:R -> R,
    continuity f <->
    (forall D:R -> Prop, open_set D -> open_set (image_rec f D)).
Proof.
  intros; split.
  intros; apply continuity_P2; assumption.
  intros; unfold continuity in |- *; unfold continuity_pt in |- *;
    unfold continue_in in |- *; unfold limit1_in in |- *;
      unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; 
        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 in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r;
    rewrite Rabs_R0; apply H0.
  apply disc_P1.
Qed.

(**********)
Theorem Rsepare :
  forall x y:R,
    x <> y ->
    exists V : R -> Prop,
      (exists W : R -> Prop,
        neighbourhood V x /\
        neighbourhood W y /\ ~ (exists y : R, intersection_domain V W y)).
Proof.
  intros x y Hsep; set (D := Rabs (x - y)).
  cut (0 < D / 2).
  intro; exists (disc x (mkposreal _ H)).
  exists (disc y (mkposreal _ H)); split.
  unfold neighbourhood in |- *; exists (mkposreal _ H); unfold included in |- *;
    tauto.
  split.
  unfold neighbourhood in |- *; exists (mkposreal _ H); unfold included in |- *;
    tauto.
  red in |- *; intro; elim H0; intros; unfold intersection_domain in H1;
    elim H1; intros.
  cut (D < D).
  intro; elim (Rlt_irrefl _ H4).
  change (Rabs (x - y) < D) in |- *;
    apply Rle_lt_trans with (Rabs (x - x0) + Rabs (x0 - y)).
  replace (x - y) with (x - x0 + (x0 - y)); [ apply Rabs_triang | ring ].
  rewrite (double_var D); apply Rplus_lt_compat.
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2.
  apply H3.
  unfold Rdiv in |- *; apply Rmult_lt_0_compat.
  unfold D in |- *; apply Rabs_pos_lt; apply (Rminus_eq_contra _ _ Hsep).
  apply Rinv_0_lt_compat; prove_sup0.
Qed.

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

Definition family_open_set (f:family) : Prop := forall x:R, open_set (f x).

Definition domain_finite (D:R -> Prop) : Prop :=
  exists l : Rlist, (forall 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 :=
  forall x:R, D x ->  exists 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 :
  forall (f:family) (D:R -> Prop) (x:R),
    (exists y : R, (fun z1 z2:R => f z1 z2 /\ D z1) x y) ->
    intersection_domain (ind f) D x.
Proof.
  intros; elim H; intros; unfold intersection_domain in |- *; 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) (fun x y:R => f x y /\ D x)
  (restriction_family f D).

Definition compact (X:R -> Prop) : Prop :=
  forall f:family,
    covering_open_set X f ->
    exists D : R -> Prop, covering_finite X (subfamily f D).

(**********)
Lemma family_P1 :
  forall (f:family) (D:R -> Prop),
    family_open_set f -> family_open_set (subfamily f D).
Proof.
  unfold family_open_set in |- *; intros; unfold subfamily in |- *;
    simpl in |- *; assert (H0 := classic (D x)).
  elim H0; intro.
  cut (open_set (f0 x) -> open_set (fun y:R => f0 x y /\ D x)).
  intro; apply H2; apply H.
  unfold open_set in |- *; unfold neighbourhood in |- *; intros; elim H3;
    intros; assert (H6 := H2 _ H4); elim H6; intros; exists x1;
      unfold included in |- *; intros; split.
  apply (H7 _ H8).
  assumption.
  cut (open_set (fun y:R => False) -> open_set (fun y:R => f0 x y /\ D x)).
  intro; apply H2; apply open_set_P4.
  unfold open_set in |- *; unfold neighbourhood in |- *; intros; elim H3;
    intros; elim H1; assumption.
Qed.

Definition bounded (D:R -> Prop) : Prop :=
  exists m : R, (exists M : R, (forall x:R, D x -> m <= x <= M)).

Lemma open_set_P6 :
  forall D1 D2:R -> Prop, open_set D1 -> D1 =_D D2 -> open_set D2.
Proof.
  unfold open_set in |- *; unfold neighbourhood in |- *; 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 : forall X:R -> Prop, compact X -> bounded X.
Proof.
  intros; unfold compact in H; set (D := fun x:R => True);
    set (g := fun x y:R => Rabs y < x);
      cut (forall x:R, (exists y : _, g x y) -> True);
        [ intro | intro; trivial ].
  set (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 in |- *; set (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 (Rabs x < r).
  intro; assert (H19 := Rabs_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 (Rabs x).
  apply RRle_abs.
  apply Rle_trans with x0.
  left; apply H11.
  assumption.
  apply (MaxRlist_P1 l x0 H16).
  unfold intersection_domain, D in |- *; tauto.
  unfold covering_open_set in |- *; split.
  unfold covering in |- *; intros; simpl in |- *; exists (Rabs x + 1);
    unfold g in |- *; pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r;
      apply Rplus_lt_compat_l; apply Rlt_0_1.
  unfold family_open_set in |- *; intro; case (Rtotal_order 0 x); intro.
  apply open_set_P6 with (disc 0 (mkposreal _ H2)).
  apply disc_P1.
  unfold eq_Dom in |- *; unfold f0 in |- *; simpl in |- *;
    unfold g, disc in |- *; split.
  unfold included in |- *; intros; unfold Rminus in H3; rewrite Ropp_0 in H3;
    rewrite Rplus_0_r in H3; apply H3.
  unfold included in |- *; intros; unfold Rminus in |- *; rewrite Ropp_0;
    rewrite Rplus_0_r; apply H3.
  apply open_set_P6 with (fun x:R => False).
  apply open_set_P4.
  unfold eq_Dom in |- *; split.
  unfold included in |- *; intros; elim H3.
  unfold included, f0 in |- *; simpl in |- *; unfold g in |- *; intros; elim H2;
    intro;
      [ rewrite <- H4 in H3; assert (H5 := Rabs_pos x0);
        elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H3))
        | assert (H6 := Rabs_pos x0); assert (H7 := Rlt_trans _ _ _ H3 H4);
          elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7)) ].
Qed.

(**********)
Lemma compact_P2 : forall X:R -> Prop, compact X -> closed_set X.
Proof.
  intros; assert (H0 := closed_set_P1 X); elim H0; clear H0; intros _ H0;
    apply H0; clear H0.
  unfold eq_Dom in |- *; split.
  apply adherence_P1.
  unfold included in |- *; unfold adherence in |- *;
    unfold point_adherent in |- *; intros; unfold compact in H;
      assert (H1 := classic (X x)); elim H1; clear H1; intro.
  assumption.
  cut (forall y:R, X y -> 0 < Rabs (y - x) / 2).
  intro; set (D := X);
    set (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y);
      cut (forall x:R, (exists y : _, g x y) -> D x).
  intro; set (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;
          set (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 <= Rabs (y0 - x) / 2).
  intro; assert (H18 := Rlt_le_trans _ _ _ H12 H17);
    cut (Rabs (y0 - x) < Rabs (y0 - x)).
  intro; elim (Rlt_irrefl _ H19).
  apply Rle_lt_trans with (Rabs (y0 - y) + Rabs (y - x)).
  replace (y0 - x) with (y0 - y + (y - x)); [ apply Rabs_triang | ring ].
  rewrite (double_var (Rabs (y0 - x))); apply Rplus_lt_compat; assumption.
  apply (MinRlist_P1 (AbsList l x) (Rabs (y0 - x) / 2)); apply AbsList_P1;
    elim (H8 y0); clear H8; intros; apply H8; unfold intersection_domain in |- *;
      split; assumption.
  assert (H11 := disc_P1 x (mkposreal alp H9)); unfold open_set in H11;
    apply H11.
  unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r;
    rewrite Rabs_R0; apply H9.
  unfold alp in |- *; 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 in |- *; split.
  unfold covering in |- *; intros; exists x0; simpl in |- *; unfold g in |- *;
    split.
  unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
    unfold Rminus in H2; apply (H2 _ H5).
  apply H5.
  unfold family_open_set in |- *; intro; simpl in |- *; unfold g in |- *;
    elim (classic (D x0)); intro.
  apply open_set_P6 with (disc x0 (mkposreal _ (H2 _ H5))).
  apply disc_P1.
  unfold eq_Dom in |- *; split.
  unfold included, disc in |- *; simpl in |- *; intros; split.
  rewrite <- (Rabs_Ropp (x0 - x1)); rewrite Ropp_minus_distr; apply H6.
  apply H5.
  unfold included, disc in |- *; simpl in |- *; intros; elim H6; intros;
    rewrite <- (Rabs_Ropp (x1 - x0)); rewrite Ropp_minus_distr; 
      apply H7.
  apply open_set_P6 with (fun z:R => False).
  apply open_set_P4.
  unfold eq_Dom in |- *; split.
  unfold included in |- *; intros; elim H6.
  unfold included in |- *; 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 in |- *; apply Rmult_lt_0_compat.
  apply Rabs_pos_lt; apply Rminus_eq_contra; red in |- *; intro;
    rewrite H3 in H2; elim H1; apply H2.
  apply Rinv_0_lt_compat; prove_sup0.
Qed.

(**********)
Lemma compact_EMP : compact (fun _:R => False).
Proof.
  unfold compact in |- *; intros; exists (fun x:R => False);
    unfold covering_finite in |- *; split.
  unfold covering in |- *; intros; elim H0.
  unfold family_finite in |- *; unfold domain_finite in |- *; exists nil; intro.
  split.
  simpl in |- *; unfold intersection_domain in |- *; intros; elim H0.
  elim H0; clear H0; intros _ H0; elim H0.
  simpl in |- *; intro; elim H0.
Qed.

Lemma compact_eqDom :
  forall X1 X2:R -> Prop, compact X1 -> X1 =_D X2 -> compact X2.
Proof.
  unfold compact in |- *; intros; unfold eq_Dom in H0; elim H0; clear H0;
    unfold included in |- *; intros; assert (H3 : covering_open_set X1 f0).
  unfold covering_open_set in |- *; unfold covering_open_set in H1; elim H1;
    clear H1; intros; split.
  unfold covering in H1; unfold covering in |- *; intros;
    apply (H1 _ (H0 _ H4)).
  apply H3.
  elim (H _ H3); intros D H4; exists D; unfold covering_finite in |- *;
    unfold covering_finite in H4; elim H4; intros; split.
  unfold covering in H5; unfold covering in |- *; intros;
    apply (H5 _ (H2 _ H7)).
  apply H6.
Qed.

(** Borel-Lebesgue's lemma *)
Lemma compact_P3 : forall a b:R, compact (fun c:R => a <= c <= b).
Proof.
  intros; case (Rle_dec a b); intro.
  unfold compact in |- *; intros;
    set
      (A :=
        fun x:R =>
          a <= x <= b /\
          (exists D : R -> Prop,
            covering_finite (fun c:R => a <= c <= x) (subfamily f0 D)));
      cut (A a).
  intro; cut (bound A).
  intro; cut (exists a0 : R, A a0).
  intro; assert (H3 := completeness 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 (exists x : R, A x /\ m - eps < x <= m).
  intro; elim H9; clear H9; intros x H9; elim H9; clear H9; intros;
    case (Req_dec 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;
      set (Db := fun x:R => Dx x \/ x = y0); exists Db;
        unfold covering_finite in |- *; split.
  unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12;
    intros; unfold covering in H12; case (Rle_dec x0 x); 
      intro.
  cut (a <= x0 <= x).
  intro; assert (H16 := H12 x0 H15); elim H16; clear H16; intros; exists x1;
    simpl in H16; simpl in |- *; unfold Db in |- *; elim H16; 
      clear H16; intros; split; [ apply H16 | left; apply H17 ].
  split.
  elim H14; intros; assumption.
  assumption.
  exists y0; simpl in |- *; split.
  apply H8; unfold disc in |- *; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr;
    rewrite Rabs_right.
  apply Rlt_trans with (b - x).
  unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar;
    auto with real.
  elim H10; intros H15 _; apply Rplus_lt_reg_r 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_ge; elim H14; intros _ H15; apply H15.
  unfold Db in |- *; right; reflexivity.
  unfold family_finite in |- *; unfold domain_finite in |- *;
    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_dec x0 y0); intro.
  simpl in |- *; left; apply H16.
  simpl in |- *; right; apply H13.
  simpl in |- *; unfold intersection_domain in |- *; unfold Db in H14;
    decompose [and or] H14.
  split; assumption.
  elim H16; assumption.
  intro; simpl in H14; elim H14; intro; simpl in |- *;
    unfold intersection_domain in |- *.
  split.
  apply (cond_fam f0); rewrite H15; exists m; apply H6.
  unfold Db in |- *; right; assumption.
  simpl in |- *; unfold intersection_domain in |- *; elim (H13 x0).
  intros _ H16; assert (H17 := H16 H15); simpl in H17;
    unfold intersection_domain in H17; split.
  elim H17; intros; assumption.
  unfold Db in |- *; left; elim H17; intros; assumption.
  set (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_irrefl _ (Rle_lt_trans _ _ _ H15 H16)).
  unfold m' in |- *; unfold Rmin in |- *; case (Rle_dec (m + eps / 2) b); intro.
  pattern m at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
    unfold Rdiv in |- *; apply Rmult_lt_0_compat;
      [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ].
  elim H4; intros.
  elim H17; intro.
  assumption.
  elim H11; assumption.
  unfold A in |- *; split.
  split.
  apply Rle_trans with m.
  elim H4; intros; assumption.
  unfold m' in |- *; unfold Rmin in |- *; case (Rle_dec (m + eps / 2) b); intro.
  pattern m at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
    unfold Rdiv in |- *; apply Rmult_lt_0_compat;
      [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ].
  elim H4; intros.
  elim H13; intro.
  assumption.
  elim H11; assumption.
  unfold m' in |- *; apply Rmin_r.
  unfold A in H9; elim H9; clear H9; intros; elim H12; clear H12; intros Dx H12;
    set (Db := fun x:R => Dx x \/ x = y0); exists Db;
      unfold covering_finite in |- *; split.
  unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12;
    intros; unfold covering in H12; case (Rle_dec x0 x); 
      intro.
  cut (a <= x0 <= x).
  intro; assert (H16 := H12 x0 H15); elim H16; clear H16; intros; exists x1;
    simpl in H16; simpl in |- *; unfold Db in |- *.
  elim H16; clear H16; intros; split; [ apply H16 | left; apply H17 ].
  elim H14; intros; split; assumption.
  exists y0; simpl in |- *; split.
  apply H8; unfold disc in |- *; unfold Rabs in |- *; case (Rcase_abs (x0 - m));
    intro.
  rewrite Ropp_minus_distr; apply Rlt_trans with (m - x).
  unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar;
    auto with real.
  apply Rplus_lt_reg_r 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 in |- *; do 2 rewrite <- (Rplus_comm (- m));
    apply Rplus_le_compat_l; elim H14; intros; assumption.
  apply Rplus_lt_reg_r with m; replace (m + (m' - m)) with m'.
  apply Rle_lt_trans with (m + eps / 2).
  unfold m' in |- *; apply Rmin_l.
  apply Rplus_lt_compat_l; apply Rmult_lt_reg_l with 2.
  prove_sup0.
  unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
    rewrite <- Rinv_r_sym.
  rewrite Rmult_1_l; pattern (pos eps) at 1 in |- *; rewrite <- Rplus_0_r;
    rewrite double; apply Rplus_lt_compat_l; apply (cond_pos eps).
  discrR.
  ring.
  unfold Db in |- *; right; reflexivity.
  unfold family_finite in |- *; unfold domain_finite in |- *;
    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_dec x0 y0); intro.
  simpl in |- *; left; apply H16.
  simpl in |- *; right; apply H13; simpl in |- *;
    unfold intersection_domain in |- *; unfold Db in H14; 
      decompose [and or] H14.
  split; assumption.
  elim H16; assumption.
  intro; simpl in H14; elim H14; intro; simpl in |- *;
    unfold intersection_domain in |- *.
  split.
  apply (cond_fam f0); rewrite H15; exists m; apply H6.
  unfold Db in |- *; 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 in |- *; left; elim H17; intros; assumption.
  elim (classic (exists 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_irrefl _ (Rle_lt_trans _ _ _ H13 H14)).
  pattern m at 2 in |- *; rewrite <- Rplus_0_r; unfold Rminus in |- *;
    apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_involutive;
      rewrite Ropp_0; apply (cond_pos eps).
  set (P := fun n:R => A n /\ m - eps < n <= m);
    assert (H12 := not_ex_all_not _ P H9); unfold P in H12;
      unfold is_upper_bound in |- *; intros;
        assert (H14 := not_and_or _ _ (H12 x)); elim H14; 
          intro.
  elim H15; apply H13.
  elim (not_and_or _ _ H15); intro.
  case (Rle_dec 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 in |- *; 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 in |- *; exists b; unfold is_upper_bound in |- *; intros;
    unfold A in H1; elim H1; clear H1; intros H1 _; elim H1; 
      clear H1; intros _ H1; apply H1.
  unfold A in |- *; 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; set (D' := fun x:R => x = y0); exists D';
    unfold covering_finite in |- *; split.
  unfold covering in |- *; simpl in |- *; intros; cut (x = a).
  intro; exists y0; split.
  rewrite H4; apply H2.
  unfold D' in |- *; reflexivity.
  elim H3; intros; apply Rle_antisym; assumption.
  unfold family_finite in |- *; unfold domain_finite in |- *;
    exists (cons y0 nil); intro; split.
  simpl in |- *; unfold intersection_domain in |- *; intro; elim H3; clear H3;
    intros; unfold D' in H4; left; apply H4.
  simpl in |- *; unfold intersection_domain in |- *; 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 (fun c:R => False).
  apply compact_EMP.
  unfold eq_Dom in |- *; split.
  unfold included in |- *; intros; elim H.
  unfold included in |- *; intros; elim H; clear H; intros;
    assert (H1 := Rle_trans _ _ _ H H0); elim n; apply H1.
Qed.

Lemma compact_P4 :
  forall X F:R -> Prop, compact X -> closed_set F -> included F X -> compact F.
Proof.
  unfold compact in |- *; intros; elim (classic (exists z : R, F z));
    intro Hyp_F_NE.
  set (D := ind f0); set (g := f f0); unfold closed_set in H0.
  set (g' := fun x y:R => f0 x y \/ complementary F y /\ D x).
  set (D' := D).
  cut (forall x:R, (exists y : R, g' x y) -> D' x).
  intro; set (f' := mkfamily D' g' H3); cut (covering_open_set X f').
  intro; elim (H _ H4); intros DX H5; exists DX.
  unfold covering_finite in |- *; unfold covering_finite in H5; elim H5;
    clear H5; intros.
  split.
  unfold covering in |- *; unfold covering in H5; intros.
  elim (H5 _ (H1 _ H7)); intros y0 H8; exists y0; simpl in H8; simpl in |- *;
    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 in |- *; unfold domain_finite in |- *;
    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 in |- *; unfold intersection_domain in |- *;
    simpl in H9; unfold intersection_domain in H9; unfold D' in |- *; 
      apply H9.
  intro; assert (H10 := H8 H9); simpl in H10; unfold intersection_domain in H10;
    simpl in |- *; unfold intersection_domain in |- *; 
      unfold D' in H10; apply H10.
  unfold covering_open_set in |- *; unfold covering_open_set in H2; elim H2;
    clear H2; intros.
  split.
  unfold covering in |- *; unfold covering in H2; intros.
  elim (classic (F x)); intro.
  elim (H2 _ H6); intros y0 H7; exists y0; simpl in |- *; unfold g' in |- *;
    left; assumption.
  cut (exists z : R, D z).
  intro; elim H7; clear H7; intros x0 H7; exists x0; simpl in |- *;
    unfold g' in |- *; right.
  split.
  unfold complementary in |- *; 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 in |- *; intro; simpl in |- *; unfold g' in |- *;
    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 in |- *; split.
  unfold included, union_domain, complementary in |- *; intros.
  elim H6; intro; [ left; apply H7 | right; split; assumption ].
  unfold included, union_domain, complementary in |- *; 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 in |- *; split.
  unfold included, complementary in |- *; intros; left; apply H6.
  unfold included, complementary in |- *; 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 (fun _:R => False).
  apply compact_EMP.
  unfold eq_Dom in |- *; split.
  unfold included in |- *; intros; elim H3.
  assert (H3 := not_ex_all_not _ _ Hyp_F_NE); unfold included in |- *; intros;
    elim (H3 x); apply H4.
Qed.

(**********)
Lemma compact_P5 : forall X:R -> Prop, closed_set X -> bounded X -> compact X.
Proof.
  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 (fun c:R => m <= c <= M) X H1 H H0).
Qed.

(**********)
Lemma compact_carac :
  forall X:R -> Prop, compact X <-> closed_set X /\ bounded X.
Proof.
  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) (x:R) : Prop :=
  exists y : R, x = f y /\ D y.

(**********)
Lemma continuity_compact :
  forall (f:R -> R) (X:R -> Prop),
    (forall x:R, continuity_pt f x) -> compact X -> compact (image_dir f X).
Proof.
  unfold compact in |- *; intros; unfold covering_open_set in H1.
  elim H1; clear H1; intros.
  set (D := ind f1).
  set (g := fun x y:R => image_rec f0 (f1 x) y).
  cut (forall x:R, (exists y : R, g x y) -> D x).
  intro; set (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 in |- *; split.
  unfold covering, image_dir in |- *; simpl in |- *; 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 in |- *; unfold domain_finite in |- *; 
      elim H6; intros l H7; exists l; intro; elim (H7 x); 
        intros; split; intro.
  apply H8; simpl in H10; simpl in |- *; apply H10.
  apply (H9 H10).
  unfold covering_open_set in |- *; split.
  unfold covering in |- *; intros; simpl in |- *; unfold covering in H1;
    unfold image_dir in H1; unfold g in |- *; unfold image_rec in |- *; 
      apply H1.
  exists x; split; [ reflexivity | apply H4 ].
  unfold family_open_set in |- *; unfold family_open_set in H2; intro;
    simpl in |- *; unfold g in |- *;
      cut ((fun 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 : forall a b:R, a < b -> 0 < b - a.
Proof.
  intros; apply Rplus_lt_reg_r with a; rewrite Rplus_0_r;
    replace (a + (b - a)) with b; [ assumption | ring ].
Qed.

Lemma prolongement_C0 :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall c:R, a <= c <= b -> continuity_pt f c) ->
    exists g : R -> R,
      continuity g /\ (forall c:R, a <= c <= b -> g c = f c).
Proof.
  intros; elim H; intro.
  set
    (h :=
      fun x:R =>
        match Rle_dec x a with
          | left _ => f0 a
          | right _ =>
            match Rle_dec x b with
              | left _ => f0 x
              | right _ => f0 b
            end
        end).
  assert (H2 : 0 < b - a).
  apply Rlt_Rminus; assumption.
  exists h; split.
  unfold continuity in |- *; intro; case (Rtotal_order x a); intro.
  unfold continuity_pt in |- *; unfold continue_in in |- *;
    unfold limit1_in in |- *; unfold limit_in in |- *; 
      simpl in |- *; unfold R_dist in |- *; intros; exists (a - x); 
        split.
  change (0 < a - x) in |- *; apply Rlt_Rminus; assumption.
  intros; elim H5; clear H5; intros _ H5; unfold h in |- *.
  case (Rle_dec x a); intro.
  case (Rle_dec x0 a); intro.
  unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
  elim n; left; apply Rplus_lt_reg_r with (- x);
    do 2 rewrite (Rplus_comm (- x)); apply Rle_lt_trans with (Rabs (x0 - x)).
  apply RRle_abs.
  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 in |- *;
        unfold continue_in in |- *; unfold limit1_in in |- *;
          unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; 
            intros; elim (H6 _ H7); intros; exists (Rmin x0 (b - a)); 
              split.
  unfold Rmin in |- *; case (Rle_dec x0 (b - a)); intro.
  elim H8; intros; assumption.
  change (0 < b - a) in |- *; apply Rlt_Rminus; assumption.
  intros; elim H9; clear H9; intros _ H9; cut (x1 < b).
  intro; unfold h in |- *; case (Rle_dec x a); intro.
  case (Rle_dec x1 a); intro.
  unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
  case (Rle_dec x1 b); intro.
  elim H8; intros; apply H12; split.
  unfold D_x, no_cond in |- *; split.
  trivial.
  red in |- *; intro; elim n; right; symmetry  in |- *; 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 Rplus_lt_reg_r with (- a); do 2 rewrite (Rplus_comm (- a));
    rewrite H4 in H9; apply Rle_lt_trans with (Rabs (x1 - a)).
  apply RRle_abs.
  apply Rlt_le_trans with (Rmin x0 (b - a)).
  assumption.
  apply Rmin_r.
  case (Rtotal_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 in |- *;
        unfold continue_in in |- *; unfold limit1_in in |- *;
          unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; 
            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 in |- *; case (Rle_dec (x - a) (b - x)); intro.
  case (Rle_dec x0 (x - a)); intro.
  assumption.
  assumption.
  case (Rle_dec x0 (b - x)); intro.
  assumption.
  assumption.
  intros; elim H13; clear H13; intros; cut (a < x1 < b).
  intro; elim H15; clear H15; intros; unfold h in |- *; case (Rle_dec x a);
    intro.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)).
  case (Rle_dec x b); intro.
  case (Rle_dec x1 a); intro.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H15)).
  case (Rle_dec 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_lt_cancel; apply Rplus_lt_reg_r with x;
    apply Rle_lt_trans with (Rabs (x1 - x)).
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs.
  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 Rplus_lt_reg_r with (- x); do 2 rewrite (Rplus_comm (- x));
    apply Rle_lt_trans with (Rabs (x1 - x)).
  apply RRle_abs.
  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 in |- *;
        unfold continue_in in |- *; unfold limit1_in in |- *;
          unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; 
            intros; elim (H8 _ H9); intros; exists (Rmin x0 (b - a)); 
              split.
  unfold Rmin in |- *; case (Rle_dec x0 (b - a)); intro.
  elim H10; intros; assumption.
  change (0 < b - a) in |- *; apply Rlt_Rminus; assumption.
  intros; elim H11; clear H11; intros _ H11; cut (a < x1).
  intro; unfold h in |- *; case (Rle_dec x a); intro.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)).
  case (Rle_dec x1 a); intro.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H12)).
  case (Rle_dec x b); intro.
  case (Rle_dec x1 b); intro.
  rewrite H6; elim H10; intros; elim r0; intro.
  apply H14; split.
  unfold D_x, no_cond in |- *; split.
  trivial.
  red in |- *; intro; rewrite <- H16 in H15; elim (Rlt_irrefl _ H15).
  rewrite H6 in H11; apply Rlt_le_trans with (Rmin x0 (b - a)).
  apply H11.
  apply Rmin_l.
  rewrite H15; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
    assumption.
  rewrite H6; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
    assumption.
  elim n1; right; assumption.
  rewrite H6 in H11; apply Ropp_lt_cancel; apply Rplus_lt_reg_r with b;
    apply Rle_lt_trans with (Rabs (x1 - b)).
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs.
  apply Rlt_le_trans with (Rmin x0 (b - a)).
  assumption.
  apply Rmin_r.
  unfold continuity_pt in |- *; unfold continue_in in |- *;
    unfold limit1_in in |- *; unfold limit_in in |- *; 
      simpl in |- *; unfold R_dist in |- *; intros; exists (x - b); 
        split.
  change (0 < x - b) in |- *; apply Rlt_Rminus; assumption.
  intros; elim H8; clear H8; intros.
  assert (H10 : b < x0).
  apply Ropp_lt_cancel; apply Rplus_lt_reg_r with x;
    apply Rle_lt_trans with (Rabs (x0 - x)).
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs.
  assumption.
  unfold h in |- *; case (Rle_dec x a); intro.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)).
  case (Rle_dec x b); intro.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H6)).
  case (Rle_dec x0 a); intro.
  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H1 (Rlt_le_trans _ _ _ H10 r))).
  case (Rle_dec x0 b); intro.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H10)).
  unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
  intros; elim H3; intros; unfold h in |- *; case (Rle_dec c a); intro.
  elim r; intro.
  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 H6)).
  rewrite H6; reflexivity.
  case (Rle_dec c b); intro.
  reflexivity.
  elim n0; assumption.
  exists (fun _: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 :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall c:R, a <= c <= b -> continuity_pt f c) ->
    exists Mx : R, (forall c:R, a <= c <= b -> f c <= f Mx) /\ a <= Mx <= b.
Proof.
  intros;
    cut
      (exists g : R -> R,
        continuity g /\ (forall 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 (fun c:R => a <= c <= b) Hcont H1).
  assert (H3 := compact_P2 _ H2).
  assert (H4 := compact_P1 _ H2).
  cut (bound (image_dir g (fun c:R => a <= c <= b))).
  cut (exists x : R, image_dir g (fun c:R => a <= c <= b) x).
  intros; assert (H7 := completeness _ H6 H5).
  elim H7; clear H7; intros M H7; cut (image_dir g (fun 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 in |- *; exists c; split; [ reflexivity | apply H10 ].
  apply H9.
  elim (classic (image_dir g (fun c:R => a <= c <= b) M)); intro.
  assumption.
  cut
    (exists eps : posreal,
      (forall y:R,
        ~
        intersection_domain (disc M eps)
        (image_dir g (fun 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 (fun c:R => a <= c <= b)) (M - eps)).
  intro; assert (H12 := H10 _ H11); cut (M - eps < M).
  intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H12 H13)).
  pattern M at 2 in |- *; rewrite <- Rplus_0_r; unfold Rminus in |- *;
    apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_0;
      rewrite Ropp_involutive; apply (cond_pos eps).
  unfold is_upper_bound, image_dir in |- *; intros; cut (x <= M).
  intro; case (Rle_dec x (M - eps)); intro.
  apply r.
  elim (H9 x); unfold intersection_domain, disc, image_dir in |- *; split.
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; rewrite Rabs_right.
  apply Rplus_lt_reg_r 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_ge; apply H12.
  apply H11.
  apply H7; apply H11.
  cut
    (exists V : R -> Prop,
      neighbourhood V M /\
      (forall y:R,
        ~ intersection_domain V (image_dir g (fun 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 in |- *; intro; elim (H11 y).
  unfold intersection_domain in |- *; unfold intersection_domain in H13;
    elim H13; clear H13; intros; split.
  apply (H12 _ H13).
  apply H14.
  cut (~ point_adherent (image_dir g (fun c:R => a <= c <= b)) M).
  intro; unfold point_adherent in H9.
  assert
    (H10 :=
      not_all_ex_not _
      (fun V:R -> Prop =>
        neighbourhood V M ->
        exists y : R,
          intersection_domain V (image_dir g (fun 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 in |- *; intro; cut (adherence (image_dir g (fun c:R => a <= c <= b)) M).
  intro; elim (closed_set_P1 (image_dir g (fun 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 in |- *; exists a; split.
  reflexivity.
  split; [ right; reflexivity | apply H ].
  unfold bound in |- *; unfold bounded in H4; elim H4; clear H4; intros m H4;
    elim H4; clear H4; intros M H4; exists M; unfold is_upper_bound in |- *;
      intros; elim (H4 _ H5); intros _ H6; apply H6.
  apply prolongement_C0; assumption.
Qed.

(**********)
Lemma continuity_ab_min :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall c:R, a <= c <= b -> continuity_pt f c) ->
    exists mx : R, (forall c:R, a <= c <= b -> f mx <= f c) /\ a <= mx <= b.
Proof.
  intros.
  cut (forall c:R, a <= c <= b -> continuity_pt (- f0) c).
  intro; assert (H2 := continuity_ab_maj (- f0)%F a b H H1); elim H2;
    intros x0 H3; exists x0; intros; split.
  intros; rewrite <- (Ropp_involutive (f0 x0));
    rewrite <- (Ropp_involutive (f0 c)); apply Ropp_le_contravar; 
      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 :=
  forall (V:R -> Prop) (N:nat),
    neighbourhood V x ->  exists p : nat, (N <= p)%nat /\ V (un p).

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

Lemma ValAdh_un_exists :
  forall (un:nat -> R) (D:=fun x:R =>  exists n : nat, x = INR n)
    (f:=
      fun x:R =>
        adherence
        (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x))
    (x:R), (exists y : R, f x y) -> D x.
Proof.
  intros; elim H; intros; unfold f in H0; unfold adherence in H0;
    unfold point_adherent in H0;
      assert (H1 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0).
  unfold neighbourhood, disc in |- *; exists (mkposreal _ Rlt_0_1);
    unfold included in |- *; 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 := fun x:R =>  exists n : nat, x = INR n in
    let f :=
      fun x:R =>
        adherence
        (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x) in
        intersection_family (mkfamily D f (ValAdh_un_exists un)).

Lemma ValAdh_un_prop :
  forall (un:nat -> R) (x:R), ValAdh un x <-> ValAdh_un un x.
Proof.
  intros; split; intro.
  unfold ValAdh in H; unfold ValAdh_un in |- *;
    unfold intersection_family in |- *; simpl in |- *; 
      intros; elim H0; intros N H1; unfold adherence in |- *;
        unfold point_adherent in |- *; intros; elim (H V N H2); 
          intros; exists (un x0); unfold intersection_domain in |- *; 
            elim H3; clear H3; intros; split.
  assumption.
  split.
  exists x0; split; [ reflexivity | rewrite H1; apply (le_INR _ _ H3) ].
  exists N; assumption.
  unfold ValAdh in |- *; intros; unfold ValAdh_un in H;
    unfold intersection_family in H; simpl in H;
      assert
        (H1 :
          adherence
          (fun y0:R =>
            (exists p : nat, y0 = un p /\ INR N <= INR p) /\
            (exists 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 :
  forall F G:R -> Prop, included F G -> included (adherence F) (adherence G).
Proof.
  unfold adherence, included in |- *; unfold point_adherent in |- *; intros;
    elim (H0 _ H1); unfold intersection_domain in |- *; 
      intros; elim H2; clear H2; intros; exists x0; split;
        [ assumption | apply (H _ H3) ].
Qed.

Definition family_closed_set (f:family) : Prop :=
  forall x:R, closed_set (f x).

Definition intersection_vide_in (D:R -> Prop) (f:family) : Prop :=
  forall x:R,
    (ind f x -> included (f x) D) /\
    ~ (exists 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 :
  forall X:R -> Prop,
    compact X ->
    (exists z : R, X z) ->
    forall g:family,
      family_closed_set g ->
      intersection_vide_in X g ->
      exists D : R -> Prop, intersection_vide_finite_in X (subfamily g D).
Proof.
  intros X H Hyp g H0 H1.
  set (D' := ind g).
  set (f' := fun x y:R => complementary (g x) y /\ D' x).
  assert (H2 : forall x:R, (exists y : R, f' x y) -> D' x).
  intros; elim H2; intros; unfold f' in H3; elim H3; intros; assumption.
  set (f0 := mkfamily D' f' H2).
  unfold compact in H; assert (H3 : covering_open_set X f0).
  unfold covering_open_set in |- *; split.
  unfold covering in |- *; intros; unfold intersection_vide_in in H1;
    elim (H1 x); intros; unfold intersection_family in H5;
      assert
        (H6 := not_ex_all_not _ (fun y:R => forall y0:R, ind g y0 -> g y0 y) H5 x);
        assert (H7 := not_all_ex_not _ (fun y0:R => ind g y0 -> g y0 x) H6); 
          elim H7; intros; exists x0; elim (imply_to_and _ _ H8); 
            intros; unfold f0 in |- *; simpl in |- *; unfold f' in |- *; 
              split; [ apply H10 | apply H9 ].
  unfold family_open_set in |- *; 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 in |- *; simpl in |- *; unfold f' in |- *; unfold eq_Dom in |- *;
    split.
  unfold included in |- *; intros; split; [ apply H4 | apply H3 ].
  unfold included in |- *; intros; elim H4; intros; assumption.
  apply open_set_P6 with (fun _:R => False).
  apply open_set_P4.
  unfold eq_Dom in |- *; unfold included in |- *; 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 in |- *; split.
  unfold intersection_vide_in in |- *; simpl in |- *; intros; split.
  intros; unfold included in |- *; 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 (exists y : R, intersection_domain (ind g) SF y)); intro Hyp'.
  red in |- *; 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 (exists 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 in |- *; 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 in |- *; unfold domain_finite in |- *; 
        elim H5; clear H5; intros l H5; exists l; intro; elim (H5 x); 
          intros; split; intro;
            [ apply H6; simpl in |- *; simpl in H8; apply H8 | apply (H7 H8) ].
Qed.

Theorem Bolzano_Weierstrass :
  forall (un:nat -> R) (X:R -> Prop),
    compact X -> (forall n:nat, X (un n)) ->  exists l : R, ValAdh un l.
Proof.
  intros; cut (exists l : R, ValAdh_un un l).
  intro; elim H1; intros; exists x; elim (ValAdh_un_prop un x); intros;
    apply (H4 H2).
  assert (H1 :  exists z : R, X z).
  exists (un 0%nat); apply H0.
  set (D := fun x:R =>  exists n : nat, x = INR n).
  set
    (g :=
      fun x:R =>
        adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)).
  assert (H2 : forall x:R, (exists 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_0_1)) x0).
  unfold neighbourhood in |- *; exists (mkposreal _ Rlt_0_1);
    unfold included in |- *; trivial.
  elim (H3 _ H4); intros; unfold intersection_domain in H5; decompose [and] H5;
    assumption.
  set (f0 := mkfamily D g H2).
  assert (H3 := compact_P6 X H H1 f0).
  elim (classic (exists 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 0); intros _ H10; elim H10; unfold family_finite in H9;
        unfold domain_finite in H9; elim H9; clear H9; intros l H9;
          set (r := MaxRlist l); cut (D r).
  intro; unfold D in H11; elim H11; intros; exists (un x);
    unfold intersection_family in |- *; simpl in |- *;
      unfold intersection_domain in |- *; intros; split.
  unfold g in |- *; apply adherence_P1; split.
  exists x; split;
    [ reflexivity
      | rewrite <- H12; unfold r in |- *; apply MaxRlist_P1; elim (H9 y); intros;
        apply H14; simpl in |- *; 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 in |- *; apply MaxRlist_P2;
    cut (exists 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 (exists z : R, intersection_domain (ind f0) SF z)); intro.
  assumption.
  elim (H8 0); intros _ H14; elim H1; intros;
    assert
      (H16 :=
        not_ex_all_not _ (fun y:R => intersection_family (subfamily f0 SF) y) H14);
      assert
        (H17 :=
          not_ex_all_not _ (fun 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 _ (fun 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 in |- *; intros; split.
  intro; simpl in H6; unfold f0 in |- *; simpl in |- *; unfold g in |- *;
    apply included_trans with (adherence X).
  apply adherence_P4.
  unfold included in |- *; 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 in |- *; unfold f0 in |- *; simpl in |- *;
    unfold g in |- *; intro; apply adherence_P3.
Qed.

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

Definition uniform_continuity (f:R -> R) (X:R -> Prop) : Prop :=
  forall eps:posreal,
    exists delta : posreal,
      (forall x y:R,
        X x -> X y -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps).

Lemma is_lub_u :
  forall (E:R -> Prop) (x y:R), is_lub E x -> is_lub E y -> x = y.
Proof.
  unfold is_lub in |- *; intros; elim H; elim H0; intros; apply Rle_antisym;
    [ apply (H4 _ H1) | apply (H2 _ H3) ].
Qed.

Lemma domain_P1 :
  forall X:R -> Prop,
    ~ (exists y : R, X y) \/
    (exists y : R, X y /\ (forall x:R, X x -> x = y)) \/
    (exists x : R, (exists y : R, X x /\ X y /\ x <> y)).
Proof.
  intro; elim (classic (exists y : R, X y)); intro.
  right; elim H; intros; elim (classic (exists y : R, X y /\ y <> x)); intro.
  right; elim H1; intros; elim H2; intros; exists x; exists x0; intros.
  split;
    [ assumption
      | split; [ assumption | apply (sym_not_eq (A:=R)); assumption ] ].
  left; exists x; split.
  assumption.
  intros; case (Req_dec x0 x); intro.
  assumption.
  elim H1; exists x0; split; assumption.
  left; assumption.
Qed.

Theorem Heine :
  forall (f:R -> R) (X:R -> Prop),
    compact X ->
    (forall x:R, X x -> continuity_pt f x) -> uniform_continuity f X.
Proof.
  intros f0 X H0 H; elim (domain_P1 X); intro Hyp.
(* X est vide *)
  unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1);
    intros; elim Hyp; exists x; assumption.
  elim Hyp; clear Hyp; intro Hyp.
(* X possède un seul élément *)
  unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1);
    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 in |- *; rewrite Rplus_opp_r;
          rewrite Rabs_R0; apply (cond_pos eps).
(* X possède au moins deux éléments distincts *)
  assert
    (X_enc :
      exists m : R, (exists M : R, (forall 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_irrefl _ (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 in |- *; intro;
        assert (H1 : forall t:posreal, 0 < t / 2).
  intro; unfold Rdiv in |- *; apply Rmult_lt_0_compat;
    [ apply (cond_pos t) | apply Rinv_0_lt_compat; prove_sup0 ].
  set
    (g :=
      fun x y:R =>
        X x /\
        (exists del : posreal,
          (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\
          is_lub
          (fun zeta:R =>
            0 < zeta <= M - m /\
            (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2))
          del /\ disc x (mkposreal (del / 2) (H1 del)) y)).
  assert (H2 : forall x:R, (exists y : R, g x y) -> X x).
  intros; elim H2; intros; unfold g in H3; elim H3; clear H3; intros H3 _;
    apply H3.
  set (f' := mkfamily X g H2); unfold compact in H0;
    assert (H3 : covering_open_set X f').
  unfold covering_open_set in |- *; split.
  unfold covering in |- *; intros; exists x; simpl in |- *; unfold g in |- *;
    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;
          set
            (E :=
              fun zeta:R =>
                0 < zeta <= M - m /\
                (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2));
            assert (H6 : bound E).
  unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *;
    unfold E in |- *; intros; elim H6; clear H6; intros H6 _; 
      elim H6; clear H6; intros _ H6; apply H6.
  assert (H7 :  exists x : R, E x).
  elim H5; clear H5; intros; exists (Rmin x0 (M - m)); unfold E in |- *; intros;
    split.
  split.
  unfold Rmin in |- *; case (Rle_dec x0 (M - m)); intro.
  apply H5.
  apply Rlt_Rminus; apply Hyp.
  apply Rmin_r.
  intros; case (Req_dec x z); intro.
  rewrite H9; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
    apply (H1 eps).
  apply H7; split.
  unfold D_x, no_cond in |- *; split; [ trivial | assumption ].
  apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H8 | apply Rmin_l ].
  assert (H8 := completeness _ H6 H7); elim H8; clear H8; intros;
    cut (0 < x1 <= M - m).
  intro; elim H8; clear H8; intros; exists (mkposreal _ H8); split.
  intros; cut (exists alp : R, Rabs (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 (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp)); intro.
  assumption.
  assert
    (H12 :=
      not_ex_all_not _ (fun alp:R => Rabs (z - x) < alp <= x1 /\ E alp) H11);
    unfold is_lub in p; elim p; intros; cut (is_upper_bound E (Rabs (z - x))).
  intro; assert (H16 := H14 _ H15);
    elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H10 H16)).
  unfold is_upper_bound in |- *; intros; unfold is_upper_bound in H13;
    assert (H16 := H13 _ H15); case (Rle_dec x2 (Rabs (z - x))); 
      intro.
  assumption.
  elim (H12 x2); split; [ split; [ auto with real | assumption ] | assumption ].
  split.
  apply p.
  unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r;
    rewrite Rabs_R0; simpl in |- *; unfold Rdiv in |- *; 
      apply Rmult_lt_0_compat; [ apply H8 | apply Rinv_0_lt_compat; prove_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 in |- *; intro; simpl in |- *; elim (classic (X x));
    intro.
  unfold g in |- *; unfold open_set in |- *; intros; elim H4; clear H4;
    intros _ H4; elim H4; clear H4; intros; elim H4; clear H4; 
      intros; unfold neighbourhood in |- *; case (Req_dec x x0); 
        intro.
  exists (mkposreal _ (H1 x1)); rewrite <- H6; unfold included in |- *; intros;
    split.
  assumption.
  exists x1; split.
  apply H4.
  split.
  elim H5; intros; apply H8.
  apply H7.
  set (d := x1 / 2 - Rabs (x0 - x)); assert (H7 : 0 < d).
  unfold d in |- *; apply Rlt_Rminus; elim H5; clear H5; intros;
    unfold disc in H7; apply H7.
  exists (mkposreal _ H7); unfold included in |- *; intros; split.
  assumption.
  exists x1; split.
  apply H4.
  elim H5; intros; split.
  assumption.
  unfold disc in H8; simpl in H8; unfold disc in |- *; simpl in |- *;
    unfold disc in H10; simpl in H10;
      apply Rle_lt_trans with (Rabs (x2 - x0) + Rabs (x0 - x)).
  replace (x2 - x) with (x2 - x0 + (x0 - x)); [ apply Rabs_triang | ring ].
  replace (x1 / 2) with (d + Rabs (x0 - x)); [ idtac | unfold d in |- *; ring ].
  do 2 rewrite <- (Rplus_comm (Rabs (x0 - x))); apply Rplus_lt_compat_l;
    apply H8.
  apply open_set_P6 with (fun _:R => False).
  apply open_set_P4.
  unfold eq_Dom in |- *; unfold included in |- *; 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
            (forall x:R,
              In x l ->
              exists del : R,
                0 < del /\
                (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\
                included (g x) (fun z:R => Rabs (z - x) < del / 2)).
  intros;
    assert
      (H7 :=
        Rlist_P1 l
        (fun x del:R =>
          0 < del /\
          (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\
          included (g x) (fun z:R => Rabs (z - x) < del / 2)) H6); 
      elim H7; clear H7; intros l' H7; elim H7; clear H7; 
        intros; set (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 (Rabs (f0 x - f0 xi) + Rabs (f0 xi - f0 y)).
  replace (f0 x - f0 y) with (f0 x - f0 xi + (f0 xi - f0 y));
  [ apply Rabs_triang | ring ].
  rewrite (double_var eps); apply Rplus_lt_compat.
  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 in |- *; apply Rmult_lt_reg_l with 2.
  prove_sup0.
  rewrite Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
  rewrite Rmult_1_r; pattern (pos_Rl l' i) at 1 in |- *; rewrite <- Rplus_0_r;
    rewrite double; apply Rplus_lt_compat_l; apply H19.
  discrR.
  assert (H19 := H8 i H17); elim H19; clear H19; intros; rewrite <- H18 in H20;
    elim H20; clear H20; intros; rewrite <- Rabs_Ropp; 
      rewrite Ropp_minus_distr; apply H20; unfold included in H21; 
        elim H13; intros; assert (H24 := H21 x H22);
          apply Rle_lt_trans with (Rabs (y - x) + Rabs (x - xi)).
  replace (y - xi) with (y - x + (x - xi)); [ apply Rabs_triang | ring ].
  rewrite (double_var (pos_Rl l' i)); apply Rplus_lt_compat.
  apply Rlt_le_trans with (D / 2).
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H12.
  unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ 2));
    apply Rmult_le_compat_l.
  left; apply Rinv_0_lt_compat; prove_sup0.
  unfold D in |- *; 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 in |- *; apply Rmult_lt_0_compat;
    [ unfold D in |- *; 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 Rinv_0_lt_compat; prove_sup0 ].
  intros; elim (H5 x); intros; elim (H8 H6); intros;
    set
      (E :=
        fun zeta:R =>
          0 < zeta <= M - m /\
          (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2));
      assert (H11 : bound E).
  unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *;
    unfold E in |- *; intros; elim H11; clear H11; intros H11 _; 
      elim H11; clear H11; intros _ H11; apply H11.
  assert (H12 :  exists 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 in |- *; 
            intros; split.
  split;
    [ unfold Rmin in |- *; case (Rle_dec x0 (M - m)); intro;
      [ apply H12 | apply Rlt_Rminus; apply Hyp ]
      | apply Rmin_r ].
  intros; case (Req_dec x z); intro.
  rewrite H16; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
    apply (H1 eps).
  apply H14; split;
    [ unfold D_x, no_cond in |- *; split; [ trivial | assumption ]
      | apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H15 | apply Rmin_l ] ].
  assert (H13 := completeness _ 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 (exists alp : R, Rabs (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 (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp)); intro.
  assumption.
  assert
    (H17 :=
      not_ex_all_not _ (fun alp:R => Rabs (z - x) < alp <= x0 /\ E alp) H16);
    unfold is_lub in p; elim p; intros; cut (is_upper_bound E (Rabs (z - x))).
  intro; assert (H21 := H19 _ H20);
    elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H15 H21)).
  unfold is_upper_bound in |- *; intros; unfold is_upper_bound in H18;
    assert (H21 := H18 _ H20); case (Rle_dec x1 (Rabs (z - x))); 
      intro.
  assumption.
  elim (H17 x1); split.
  split; [ auto with real | assumption ].
  assumption.
  unfold included, g in |- *; 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.