CoRN.reals.Intervals

Require Export CSetoidInc.
Require Export RealLists.
Set Automatic Introduction.

Section Intervals.

Intervals

In this section we define (compact) intervals of the real line and some useful functions to work with them.

Definitions

We start by defining the compact interval [a,b] as being the set of points less or equal than b and greater or equal than a. We require a [<=] b, as we want to work only in nonempty intervals.

Definition compact (a b : IR) (Hab : a [<=] b) (x : IR) := a [<=] x and x [<=] b.

Let a,b : IR and Hab : a [<=] b.

As expected, both a and b are members of [a,b]. Also they are members of the interval [Min(a,b),Max(a,b)].

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Lemma compact_inc_lft : compact a b Hab a.
Proof.
intros; split; [ apply leEq_reflexive | auto ].
Qed.

Lemma compact_inc_rht : compact a b Hab b.
Proof.
intros; split; [ auto | apply leEq_reflexive ].
Qed.

Lemma compact_Min_lft : ∀ Hab', compact (Min a b) (Max a b) Hab' a.
Proof.
split; [ apply Min_leEq_lft | apply lft_leEq_Max ].
Qed.

Lemma compact_Min_rht : ∀ Hab', compact (Min a b) (Max a b) Hab' b.
Proof.
split; [ apply Min_leEq_rht | apply rht_leEq_Max ].
Qed.

As we will be interested in taking functions with domain in a compact interval, we want this predicate to be well defined.

Lemma compact_wd : pred_wd IR (compact a b Hab).
Proof.
intros; red in |- *; intros x y H H0.
inversion_clear H; split.
apply leEq_wdr with x; assumption.
apply leEq_wdl with x; assumption.
Qed.

Also, it will sometimes be necessary to rewrite the endpoints of an interval.

Lemma compact_wd' : ∀ (a' b' : IR) Hab' (x : IR),
a [=] a' → b [=] b' → compact a b Hab x → compact a' b' Hab' x.
Proof.
intros a' b' Hab' x H H0 H1.
inversion_clear H1; split.
apply leEq_wdl with a; auto.
apply leEq_wdr with b; auto.
Qed.

As we identify subsets with predicates, inclusion is simply implication.

Finally, we define a restriction operator that takes a function F and a well defined predicate P included in the domain of F and returns the restriction of F to P.

Definition Frestr F P (HP : pred_wd IR P) (H : included P (Dom F)) : PartIR.
Proof.
intros.
apply Build_PartFunct with P (fun (x : IR) (Hx : P x) ⇒ Part F x (H x Hx)).
assumption.
intros. exact (pfstrx _ _ _ _ _ _ X).
Defined.

End Intervals.

Notation Compact := (compact _ _).
Implicit Arguments Frestr [F P].
Notation FRestr := (Frestr (compact_wd _ _ _)).

Section More_Intervals.

Lemma included_refl' : ∀ a b Hab Hab', included (compact a b Hab) (compact a b Hab').
Proof.
intros.
red in |- *; intros x H.
inversion_clear H; split; auto.
Qed.

We prove some inclusions of compact intervals.

Definition compact_map1 : ∀ a b Hab Hab',
included (compact (Min a b) (Max a b) Hab') (compact a b Hab).
Proof.
intros.
red in |- *; intros x H.
red in |- *; red in H.
inversion_clear H.
split.
  eapply leEq_wdl; [ apply H0 | apply leEq_imp_Min_is_lft; auto ].
eapply leEq_wdr; [ apply H1 | apply leEq_imp_Max_is_rht; auto ].
Defined.

Definition compact_map2 : ∀ a b Hab Hab',
included (compact a b Hab) (compact (Min a b) (Max a b) Hab').
Proof.
intros.
red in |- *; intros x H.
red in |- *; red in H.
inversion_clear H.
split.
  eapply leEq_transitive; [ apply Min_leEq_lft | apply H0 ].
eapply leEq_transitive; [ apply H1 | apply rht_leEq_Max ].
Defined.

Definition compact_map3 : ∀ a b e Hab Hab', [0] [<] e →
included (compact a (b [-]e) Hab') (compact a b Hab).
Proof.
intros; red in |- ×. try rename X into H.
intros x H0. inversion_clear H0; split.
auto.
eapply leEq_transitive.
  apply H2.
apply shift_minus_leEq.
apply shift_leEq_plus'.
astepl ZeroR; apply less_leEq; assumption.
Qed.

End More_Intervals.

Hint Resolve included_refl' compact_map1 compact_map2 compact_map3 : included.

Section Totally_Bounded.

Totally Bounded

Totally bounded sets will play an important role in what is to come. The definition (equivalent to the classical one) states that P is totally bounded iff ∀e>0 ∃x₁,...,x_n∀y∈P∃ 1≤i≤n.|y-x_i|<e.

Notice the use of lists for quantification.

Definition totally_bounded (P : IR → CProp) : CProp := {x : IR | P x} and (∀ e,
[0] [<] e → {l : list IR | ∀ x, member x l → P x |
∀ x, P x → {y : IR | member y l | AbsSmall e (x [-]y)}}).

This definition is classically, but not constructively, equivalent to the definition of compact (if completeness is assumed); the next result, classically equivalent to the Heine-Borel theorem, justifies that we take the definition of totally bounded to be the relevant one and that we defined compacts as we did.

Lemma compact_is_totally_bounded : ∀ a b Hab, totally_bounded (compact a b Hab).
Proof.
intros; split.
  ∃ a.
  apply compact_inc_lft.
cut (∀ (n : nat) (a b e : IR) (Hab : a [<=] b) (He : [0] [<] e),
   (b [-]a [/] e [//]pos_ap_zero _ _ He ) [<=] nring n →
     (2 ≤ n → nring n [-]Two [<=] (b [-]a [/] e [//]pos_ap_zero _ _ He )) →
       {l : list IR | ∀ x : IR, member x l → compact a b Hab x | ∀ x : IR,
         compact a b Hab x → {y : IR | member y l | AbsIR (x [-]y) [<=] e }}).
  intros H e He.
  elim (str_Archimedes (b[-]a[/] _[//]pos_ap_zero _ _ (pos_div_two _ _ He))).
   intros n Hn.
   inversion_clear Hn.
   elim (H n a b _ Hab (pos_div_two _ _ He)).
     intros l Hl' Hl.
     2: assumption.
    2: assumption.
   ∃ l.
    assumption.
   intros x Hx; elim (Hl x Hx).
   intros y Hy Hy'.
   ∃ y.
    assumption.
   apply AbsIR_imp_AbsSmall.
   apply leEq_transitive with (e [/]TwoNZ).
    assumption.
   apply less_leEq; apply pos_div_two'; assumption.
  apply shift_leEq_div; [ apply pos_div_two; assumption | apply shift_leEq_minus ].
  rstepl a; assumption.
clear Hab a b; intro n; induction n as [| n Hrecn].
  intros.
  ∃ (a::nil).
   intros x H1.
   inversion H1 as [H2 | H2]. elim H2.
   apply compact_wd with a; algebra.
   apply compact_inc_lft.
  intros.
  ∃ a.
   right; algebra.
  apply leEq_wdl with ZeroR.
   apply less_leEq; auto.
  astepl (AbsIR [0]).
  apply AbsIR_wd.
  apply leEq_imp_eq. try rename X into H1.
   apply shift_leEq_minus; astepl a; elim H1; auto.
  apply shift_minus_leEq.
  apply leEq_transitive with b. try rename X into H1.
   elim H1; auto.
  apply shift_leEq_plus.
  apply mult_cancel_leEq with ([1][/] _[//]pos_ap_zero _ _ He).
   apply recip_resp_pos; auto.
  astepr ZeroR.
  rstepl (b[-]a[/] _[//]pos_ap_zero _ _ He); auto.
clear Hrecn; induction n as [| n Hrecn].
  intros.
  ∃ (a::nil).
   intros x H1.
   inversion_clear H1 as [H2|].
    elim H2.
   apply compact_wd with a; [ apply compact_inc_lft | algebra ].
  intros x Hx; inversion_clear Hx.
  ∃ a.
   simpl in |- *; right; algebra.
  eapply leEq_wdl.
   2: apply eq_symmetric_unfolded; apply AbsIR_eq_x.
   apply leEq_transitive with (b[-]a).
    apply minus_resp_leEq; assumption.
   rstepr (e[*]nring 1); eapply shift_leEq_mult'; [ assumption | apply H ].
  apply shift_leEq_minus; astepl a.
  assumption.
clear Hrecn; induction n as [| n Hrecn].
  intros.
  set (enz := pos_ap_zero _ _ He) in ×.
  ∃ (cons ((a[+]b) [/]TwoNZ) (@nil IR)).
   intros x H1.
   inversion_clear H1 as [H2|].
    inversion_clear H2.
   apply compact_wd with ((a[+]b) [/]TwoNZ); [ split | algebra ].
    astepl (a[+][0]); apply shift_plus_leEq'.
    apply mult_cancel_leEq with (Two:IR).
     apply pos_two.
    astepl ZeroR.
    rstepr (b[-]a).
    apply shift_leEq_minus; astepl a; auto.
   astepr (b[+][0]); apply shift_leEq_plus'.
   apply mult_cancel_leEq with (Two:IR).
    apply pos_two.
   astepr ZeroR.
   rstepl (a[-]b).
   apply shift_minus_leEq; astepr b; auto.
  intros.
  ∃ ((a[+]b) [/]TwoNZ).
   right; algebra.
  eapply leEq_wdl.
   2: apply eq_symmetric_unfolded; apply Abs_Max.
  apply shift_minus_leEq; apply Max_leEq; apply shift_leEq_plus'; apply leEq_Min.
     apply shift_minus_leEq; apply shift_leEq_plus'.
     astepl ZeroR; apply less_leEq; auto.
    apply shift_minus_leEq.
    apply leEq_transitive with b. try rename X into H1.
     elim H1; auto.
    apply shift_leEq_plus'.
    apply mult_cancel_leEq with (Two:IR).
     apply pos_two.
    apply shift_leEq_mult' with enz.
     auto.
    rstepl (b[-]a[/] e[//]enz); auto.
   apply leEq_transitive with a.
    2: try rename X into H1; elim H1; auto.
   apply shift_minus_leEq; apply shift_leEq_plus'.
   apply mult_cancel_leEq with (Two:IR).
    apply pos_two.
   apply shift_leEq_mult' with enz.
    auto.
   rstepl (b[-]a[/] e[//]enz); auto.
  apply shift_minus_leEq; apply shift_leEq_plus'.
  astepl ZeroR; apply less_leEq; auto.
intros.
set (b' := b[-]e) in ×.
cut (a [<=] b'); intros.
  elim (Hrecn a b' e H1 He).
    intros l Hl' Hl.
    ∃ (cons b' l).
     intros.
     unfold b' in H1; apply compact_map3 with (e := e) (Hab' := H1) (b := b).
      assumption. try rename X into H2.
     simpl in H2; inversion_clear H2.
      apply Hl'; assumption.
     apply compact_wd with b'; [ apply compact_inc_rht | algebra ].
    intros.
    cut (x [<] b' or b'[-]e [<] x). intros H3.
     inversion_clear H3.
      cut (compact a b' H1 x). intros H3.
       elim (Hl x H3).
       intros y Hy Hy'.
       ∃ y.
        left; assumption.
       auto. try rename X into H2.
      inversion_clear H2; split.
       assumption.
      apply less_leEq; auto.
     ∃ b'.
      right; algebra.
     simpl in |- *; unfold ABSIR in |- ×.
     apply Max_leEq.
      apply shift_minus_leEq; unfold b' in |- ×.
      rstepr b. try rename X into H2.
      elim H2; auto.
     rstepl (b'[-]x); apply shift_minus_leEq; apply shift_leEq_plus'; apply less_leEq; assumption.
    cut (b'[-]e [<] x or x [<] b'); [ tauto | apply less_cotransitive_unfolded ].
    apply shift_minus_less; apply shift_less_plus'; astepl ZeroR; assumption.
   unfold b' in |- ×.
   rstepl ((b[-]a[/] e[//]pos_ap_zero _ _ He) [-][1]).
   apply shift_minus_leEq.
   astepr (nring (R:=IR) (S (S (S n)))); auto.
  intro.
  unfold b' in |- ×.
  rstepr ((b[-]a[/] e[//]pos_ap_zero _ _ He) [-][1]).
  apply shift_leEq_minus.
  rstepl (nring (R:=IR) (S (S n)) [+][1][-]Two).
  auto with arith.
unfold b' in |- ×.
apply shift_leEq_minus; apply shift_plus_leEq'.
astepl ([1][*]e); apply shift_mult_leEq with (pos_ap_zero _ _ He).
  auto.
apply leEq_transitive with (nring (R:=IR) (S (S (S n))) [-]Two).
  apply shift_leEq_minus; rstepl (Three:IR); apply nring_leEq; auto with arith.
auto with arith.
Qed.

Suprema and infima will be needed throughout; we define them here both for arbitrary subsets of IR and for images of functions.

Definition set_glb_IR (P : IR → CProp) a : CProp := (∀ x, P x → a [<=] x ) and
(∀ e, [0] [<] e → {x : IR | P x | x[-]a [<] e }).

Definition set_lub_IR (P : IR → CProp) a : CProp := (∀ x, P x → x [<=] a ) and
(∀ e, [0] [<] e → {x : IR | P x | a [-]x [<] e }).

Definition fun_image F (P : IR → CProp) x : CProp := {y : IR |
P y and Dom F y and (∀ Hy, F y Hy [=] x )}.

Definition fun_glb_IR F (P : IR → CProp) a : CProp :=
set_glb_IR (fun_image F P) a.

Definition fun_lub_IR F (P : IR → CProp) a : CProp :=
set_lub_IR (fun_image F P) a.

The following are probably the most important results in this section.

Lemma totally_bounded_has_lub : ∀ P,
totally_bounded P → {z : IR | set_lub_IR P z}.
Proof.
intros P tot_bnd.
red in tot_bnd.
elim tot_bnd; intros non_empty H.
cut {sequence : nat → IR | ∀ k : nat, P (sequence k) |
   ∀ (k : nat) (x : IR), P x → x [-]sequence k [<=] Two [*]one_div_succ k }.
  intros H0.
  elim H0.
  intros seq Hseq Hseq'.
  cut (Cauchy_prop seq).
   intro H1.
   set (seq1 := Build_CauchySeq IR seq H1) in ×.
   ∃ (Lim seq1).
   split; intros.
    apply shift_leEq_rht.
    astepl ( [--]ZeroR); rstepr ( [--] (x[-]Lim seq1)).
    apply inv_resp_leEq.
    set (seq2 := Cauchy_const x) in ×.
    apply leEq_wdl with (Lim seq2[-]Lim seq1).
     2: apply cg_minus_wd; [ unfold seq2 in |- *; apply eq_symmetric_unfolded; apply Lim_const
       | algebra ].
    apply leEq_wdl with (Lim (Build_CauchySeq IR (fun n : nat ⇒ seq2 n [-]seq1 n)
      (Cauchy_minus seq2 seq1))).
     apply leEq_transitive with (Lim twice_inv_seq).
      apply Lim_leEq_Lim; intro; simpl in |- ×.
      apply Hseq'; assumption.
     apply eq_imp_leEq.
     apply eq_symmetric_unfolded; apply Limits_unique.
     red in |- *; fold (SeqLimit twice_inv_seq [0]) in |- ×.
     apply twice_inv_seq_Lim.
    apply Lim_minus.
   cut (Cauchy_Lim_prop2 seq (Lim seq1)).
    intro H4; red in H4. try rename X into H2.
    elim (H4 (e [/]TwoNZ) (pos_div_two _ _ H2)); clear H4.
    intros n Hn.
    ∃ (seq n).
     apply Hseq.
    apply leEq_less_trans with (AbsIR (Lim seq1[-]seq n)).
     apply leEq_AbsIR.
    apply leEq_less_trans with (e [/]TwoNZ).
     apply AbsSmall_imp_AbsIR.
     apply AbsSmall_minus; simpl in |- *; apply Hn.
     apply le_n.
    apply pos_div_two'; auto.
   cut (Cauchy_Lim_prop2 seq1 (Lim seq1)); intros.
    try rename X0 into H3.
    red in |- *; red in H3.
    intros eps Heps; elim (H3 eps Heps); clear H3; intros.
    ∃ x.
    intros m Hm; elim (p m Hm); clear p.
    intros.
    astepr (seq1 m[-]Lim seq1).
    apply AbsIR_eq_AbsSmall; assumption.
   red in |- *; fold (SeqLimit seq1 (Lim seq1)) in |- ×.
   apply ax_Lim.
   apply crl_proof.
  red in |- *; intros. try rename X into H1.
  elim (Archimedes ([1][/] e[//]pos_ap_zero _ _ H1)).
  intros n Hn.
  ∃ (S (2 × n)); intros.
  cut ([0] [<] nring (R:=IR) n); intros.
   apply AbsIR_eq_AbsSmall. try rename X into H3.
    apply leEq_transitive with ( [--] ([1][/] nring n[//]pos_ap_zero _ _ H3)).
     apply inv_resp_leEq.
     apply shift_div_leEq.
      assumption.
     eapply shift_leEq_mult'; [ assumption | apply Hn ].
    rstepr ( [--] (seq (S (2 × n)) [-]seq m)); apply inv_resp_leEq.
    apply leEq_transitive with (Two [*]one_div_succ (R:=IR) m).
     auto.
    apply leEq_transitive with (one_div_succ (R:=IR) n).
     unfold one_div_succ in |- ×.
     unfold Snring in |- ×.
     rstepl ([1][/] nring (S m) [/]TwoNZ [//]
       div_resp_ap_zero_rev _ _ _ _ (nring_ap_zero IR (S m) (sym_not_eq (O_S m)))).
     apply recip_resp_leEq.
      apply pos_nring_S.
     apply shift_leEq_div.
      apply pos_two.
     simpl in |- *; fold (Two:IR) in |- ×.
     rstepl (Two [*]nring (R:=IR) n[+][1][+][1]).
     apply plus_resp_leEq.
     apply leEq_wdl with (nring (R:=IR) (S (2 × n))).
      apply nring_leEq; assumption.
     Step_final (nring (R:=IR) (2 × n) [+][1]).
    unfold one_div_succ in |- *; unfold Snring in |- *; apply recip_resp_leEq.
     assumption.
    simpl in |- *; apply less_leEq; apply less_plusOne.
   apply leEq_transitive with (Two [*]one_div_succ (R:=IR) (S (2 × n))).
    auto.
   apply less_leEq. try rename X into H3.
   apply less_leEq_trans with ([1][/] nring n[//]pos_ap_zero _ _ H3).
    astepl (one_div_succ (R:=IR) (S (2 × n)) [*]Two).
    unfold one_div_succ in |- *; unfold Snring in |- ×.
    apply shift_mult_less with (two_ap_zero IR).
     apply pos_two.
    rstepr ([1][/] Two [*]nring n[//] mult_resp_ap_zero _ _ _ (two_ap_zero IR) (pos_ap_zero _ _ H3)).
    apply recip_resp_less.
     astepl (ZeroR [*][0]); apply mult_resp_less_both; try apply leEq_reflexive;
       [ apply pos_two | assumption ].
    apply less_wdr with (Two [*]nring (R:=IR) n[+][1][+][1]).
     apply less_transitive_unfolded with (Two [*]nring (R:=IR) n[+][1]); apply less_plusOne.
    astepr (nring (R:=IR) (S (2 × n)) [+][1]).
    Step_final (nring (R:=IR) (2 × n) [+][1][+][1]).
   rstepr ([1][/] [1][/] e[//]pos_ap_zero _ _ H1[//] div_resp_ap_zero_rev _ _ _ _ (one_ap_zero IR)).
   apply recip_resp_leEq; [ apply recip_resp_pos; assumption | assumption ].
  eapply less_leEq_trans.
   2: apply Hn.
  apply recip_resp_pos; assumption.
elim (aux_seq_lub_prop P tot_bnd).
∃ (fun k : nat ⇒ scs_elem _ _ (aux_seq_lub P tot_bnd k)); auto.
Qed.

Lemma totally_bounded_has_glb : ∀ P : IR → CProp,
totally_bounded P → {z : IR | set_glb_IR P z}.
Proof.
intros P tot_bnd.
red in tot_bnd.
elim tot_bnd; intros non_empty H.
cut {sequence : nat → IR | ∀ k : nat, P (sequence k) |
   ∀ (k : nat) (x : IR), P x → sequence k [-]x [<=] Two [*]one_div_succ k }.
  intros H0.
  elim H0.
  clear H0; intros seq H0 H1.
  cut (Cauchy_prop seq).
   intro H2.
   set (seq1 := Build_CauchySeq IR seq H2) in ×.
   ∃ (Lim seq1).
   split; intros.
    apply shift_leEq_rht.
    astepl ( [--]ZeroR); rstepr ( [--] (Lim seq1[-]x)).
    apply inv_resp_leEq.
    set (seq2 := Cauchy_const x) in ×.
    apply leEq_wdl with (Lim seq1[-]Lim seq2).
     2: apply cg_minus_wd; [ algebra
       | unfold seq2 in |- *; apply eq_symmetric_unfolded; apply Lim_const ].
    apply leEq_wdl with (Lim (Build_CauchySeq IR (fun n : nat ⇒ seq1 n [-]seq2 n)
      (Cauchy_minus seq1 seq2))).
     apply leEq_transitive with (Lim twice_inv_seq).
      apply Lim_leEq_Lim; intro.
      simpl in |- ×.
      apply H1; assumption.
     apply eq_imp_leEq.
     apply eq_symmetric_unfolded; apply Limits_unique.
     red in |- *; fold (SeqLimit twice_inv_seq [0]) in |- ×.
     apply twice_inv_seq_Lim.
    apply Lim_minus.
   cut (Cauchy_Lim_prop2 seq (Lim seq1)).
    intro H4; red in H4. try rename X into H3.
    elim (H4 (e [/]TwoNZ) (pos_div_two _ _ H3)); clear H4.
    intros n Hn.
    ∃ (seq n).
     apply H0.
    apply leEq_less_trans with (AbsIR (Lim seq1[-]seq n)).
     rstepl ( [--] (Lim seq1[-]seq n)).
     apply inv_leEq_AbsIR.
    apply leEq_less_trans with (e [/]TwoNZ).
     apply AbsSmall_imp_AbsIR.
     apply AbsSmall_minus; simpl in |- *; apply Hn.
     apply le_n.
    apply pos_div_two'; auto.
   cut (Cauchy_Lim_prop2 seq1 (Lim seq1)); intros.
    try rename X0 into H4.
    red in |- *; red in H4.
    intros eps Heps; elim (H4 eps Heps); clear H4; intros.
    ∃ x.
    intros m Hm; elim (p m Hm); clear p.
    intros.
    astepr (seq1 m[-]Lim seq1).
    apply AbsIR_eq_AbsSmall; assumption.
   red in |- *; fold (SeqLimit seq1 (Lim seq1)) in |- ×.
   apply ax_Lim.
   apply crl_proof.
  red in |- *; intros e H2.
  elim (Archimedes ([1][/] e[//]pos_ap_zero _ _ H2)).
  intros n Hn.
  ∃ (S (2 × n)); intros.
  cut ([0] [<] nring (R:=IR) n); intros.
   apply AbsIR_eq_AbsSmall.
    try rename X into H4.
    apply leEq_transitive with ( [--] ([1][/] nring n[//]pos_ap_zero _ _ H4)).
     apply inv_resp_leEq.
     apply shift_div_leEq.
      assumption.
     eapply shift_leEq_mult'; [ assumption | apply Hn ].
    apply less_leEq.
    rstepr ( [--] (seq (S (2 × n)) [-]seq m)); apply inv_resp_less.
    apply leEq_less_trans with (Two [*]one_div_succ (R:=IR) (S (2 × n))).
     apply H1; apply H0.
    astepl (one_div_succ (R:=IR) (S (2 × n)) [*]Two).
    unfold one_div_succ in |- *; unfold Snring in |- ×.
    apply shift_mult_less with (two_ap_zero IR).
     apply pos_two.
    rstepr ([1][/] Two [*]nring n[//] mult_resp_ap_zero _ _ _ (two_ap_zero IR) (pos_ap_zero _ _ H4)).
    apply recip_resp_less.
     astepl (ZeroR [*][0]); apply mult_resp_less_both; try apply leEq_reflexive;
       [ apply pos_two | assumption ].
    apply less_wdr with (Two [*]nring (R:=IR) n[+][1][+][1]).
     apply less_transitive_unfolded with (Two [*]nring (R:=IR) n[+][1]); apply less_plusOne.
    astepr (nring (R:=IR) (S (2 × n)) [+][1]).
    Step_final (nring (R:=IR) (2 × n) [+][1][+][1]).
   apply leEq_transitive with (Two [*]one_div_succ (R:=IR) m).
    apply H1; apply H0.
   apply leEq_transitive with (one_div_succ (R:=IR) n).
    unfold one_div_succ in |- ×.
    unfold Snring in |- ×.
    rstepl ([1][/] nring (R:=IR) (S m) [/]TwoNZ [//]
      div_resp_ap_zero_rev _ _ _ _ (nring_ap_zero IR (S m) (sym_not_eq (O_S m)))).
    apply recip_resp_leEq.
     apply pos_nring_S.
    apply shift_leEq_div.
     apply pos_two.
    simpl in |- *; fold (Two:IR) in |- ×.
    rstepl (Two [*]nring (R:=IR) n[+][1][+][1]).
    apply plus_resp_leEq.
    apply leEq_wdl with (nring (R:=IR) (S (2 × n))).
     apply nring_leEq; assumption.
    Step_final (nring (R:=IR) (2 × n) [+][1]).
   unfold one_div_succ in |- *; unfold Snring in |- ×.
   rstepr ([1][/] [1][/] e[//]pos_ap_zero _ _ H2[//] div_resp_ap_zero_rev _ _ _ _ (one_ap_zero IR)).
   apply recip_resp_leEq.
    apply recip_resp_pos; assumption.
   apply leEq_transitive with (nring (R:=IR) n);
     [ assumption | simpl in |- *; apply less_leEq; apply less_plusOne ].
  eapply less_leEq_trans.
   2: apply Hn.
  apply recip_resp_pos; assumption.
elim (aux_seq_glb_prop P tot_bnd).
∃ (fun k : nat ⇒ scs_elem _ _ (aux_seq_glb P tot_bnd k)); auto.
Qed.

End Totally_Bounded.

Section Compact.

Compact sets

In this section we dwell a bit farther into the definition of compactness and explore some of its properties.

The following characterization of inclusion can be very useful:

Lemma included_compact : ∀ (a b c d : IR) Hab Hcd, compact a b Hab c →
compact a b Hab d → included (compact c d Hcd) (compact a b Hab).
Proof.
intros a b c d Hab Hcd H H0 x H1.
inversion_clear H.
inversion_clear H0.
inversion_clear H1.
split.
apply leEq_transitive with c; auto.
apply leEq_transitive with d; auto.
Qed.

At several points in our future development of a theory we will need to partition a compact interval in subintervals of length smaller than some predefined value eps. Although this seems a consequence of every compact interval being totally bounded, it is in fact a stronger property. In this section we perform that construction (requiring the endpoints of the interval to be distinct) and prove some of its good properties.

Let a,b : IR, Hab : (a [<=] b) and denote by I the compact interval [a,b]. Also assume that a [<] b, and let e be a positive real number.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Hypothesis Hab' : a [<] b.

Variable e : IR.
Hypothesis He : [0] [<] e.

We start by finding a natural number n such that (b[-]a) [/] n [<] e.

Definition compact_nat := ProjT1 (Archimedes (b [-]a [/] e [//]pos_ap_zero _ _ He)).

Obviously such an n must be greater than zero.

Lemma pos_compact_nat : [0] [<] nring (R:=IR) compact_nat.
Proof.
apply less_leEq_trans with (b [-]a [/] e [//]pos_ap_zero _ _ He).
  rstepr ((b [-]a ) [*] ([1][/] e [//]pos_ap_zero _ _ He )).
  apply mult_resp_pos.
   apply shift_less_minus; astepl a; assumption.
  apply recip_resp_pos; assumption.
unfold compact_nat in |- *; apply proj2_sigT.
Qed.

We now define a sequence on n points in [a,b] by x_i [=] Min(a,b) [+]i[*] (b[-]a) [/]n and prove that all of its points are really in that interval.

Definition compact_part (i : nat) : i ≤ compact_nat → IR.
Proof.
intros.
apply (a [+]nring i[*] (b [-]a [/] _[//]pos_ap_zero _ _ pos_compact_nat )).
Defined.

Lemma compact_part_hyp : ∀ i Hi, compact a b Hab (compact_part i Hi).
Proof.
intros; unfold compact_part in |- ×.
split.
  astepl (a [+][0]); apply plus_resp_leEq_lft.
  astepl (ZeroR [*][0]); apply mult_resp_leEq_both; try apply leEq_reflexive.
   apply nring_nonneg.
  apply shift_leEq_div.
   apply pos_compact_nat.
  apply shift_leEq_minus; rstepl a; apply less_leEq; assumption.
rstepr (a [+]nring compact_nat [*] (b [-]a [/] _[//]pos_ap_zero _ _ pos_compact_nat )).
apply plus_resp_leEq_lft.
apply mult_resp_leEq_rht; try apply nring_nonneg.
  apply nring_leEq; assumption.
apply shift_leEq_div.
  apply pos_compact_nat.
apply shift_leEq_minus; rstepl a; apply less_leEq; assumption.
Qed.

This sequence is strictly increasing and each two consecutive points are apart by less than e.

Lemma compact_less : ∀ i Hi HSi, [0] [<] compact_part (S i) HSi [-]compact_part i Hi.
Proof.
intros i H1 H2.
apply shift_less_minus; astepl (compact_part _ H1).
unfold compact_part in |- ×.
apply plus_resp_less_lft.
apply mult_resp_less.
  simpl in |- *; apply less_plusOne.
apply div_resp_pos.
  apply pos_compact_nat.
apply shift_less_minus; astepl a; assumption.
Qed.

Lemma compact_leEq : ∀ i Hi HSi, compact_part (S i) HSi [-]compact_part i Hi [<=] e.
Proof.
intros i H1 H2.
unfold compact_part in |- *; simpl in |- ×.
rstepl (b [-]a [/] _[//]pos_ap_zero _ _ pos_compact_nat).
apply shift_div_leEq.
  apply pos_compact_nat.
apply shift_leEq_mult' with (pos_ap_zero _ _ He).
  assumption.
exact (ProjT2 (Archimedes _)).
Qed.

When we proceed to integration, this lemma will also be useful:

Lemma compact_partition_lemma : ∀ n Hn i, i ≤ n →
Compact Hab (a [+]nring i [*] (b [-]a [/] _[//]nring_ap_zero' _ n Hn )).
Proof.
intros n Hn i H; split.
  apply shift_leEq_plus'.
  astepl ZeroR.
  apply mult_resp_nonneg.
   apply nring_nonneg.
  apply shift_leEq_div.
   apply nring_pos; apply neq_O_lt; auto.
  apply shift_leEq_minus.
  rstepl a; assumption.
apply shift_plus_leEq'.
rstepr (nring n[*] (b [-]a [/] _[//]nring_ap_zero' _ _ Hn)).
astepl ([0][+]nring i[*] (b [-]a [/] _[//]nring_ap_zero' _ _ Hn)).
apply shift_plus_leEq.
rstepr ((nring n[-]nring i) [*] (b [-]a [/] _[//]nring_ap_zero' _ _ Hn)).
apply mult_resp_nonneg.
  apply shift_leEq_minus.
  astepl (nring (R:=IR) i).
  apply nring_leEq; assumption.
apply shift_leEq_div.
  apply nring_pos; apply neq_O_lt; auto.
apply shift_leEq_minus.
rstepl a; assumption.
Qed.

The next lemma provides an upper bound for the distance between two points in an interval:

Lemma compact_elements : ∀ x y : IR,
Compact Hab x → Compact Hab y → AbsIR (x [-]y) [<=] AbsIR (b [-]a).
Proof.
clear Hab' He e.
do 2 intro; intros Hx Hy.
apply leEq_wdr with (b [-]a).
  2: apply eq_symmetric_unfolded; apply AbsIR_eq_x.
  2: apply shift_leEq_minus; astepl a; auto.
eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply Abs_Max.
inversion_clear Hx.
inversion_clear Hy.
unfold cg_minus in |- *; apply plus_resp_leEq_both.
  apply Max_leEq; auto.
apply inv_resp_leEq.
apply leEq_Min; auto.
Qed.

Opaque Min Max.

The following is a variation on the previous lemma:

Lemma compact_elements' : ∀ c d Hcd x y, Compact Hab x →
compact c d Hcd y → AbsIR (x [-]y) [<=] AbsIR (Max b d [-]Min a c).
Proof.
do 5 intro; intros Hx Hy.
eapply leEq_transitive.
  2: apply leEq_AbsIR.
inversion_clear Hx.
inversion_clear Hy.
simpl in |- *; unfold ABSIR in |- *; apply Max_leEq.
  unfold cg_minus in |- *; apply plus_resp_leEq_both.
   apply leEq_transitive with b; auto; apply lft_leEq_Max.
  apply inv_resp_leEq; apply leEq_transitive with c; auto; apply Min_leEq_rht.
rstepl (y[-]x).
unfold cg_minus in |- *; apply plus_resp_leEq_both.
  apply leEq_transitive with d; auto; apply rht_leEq_Max.
apply inv_resp_leEq; apply leEq_transitive with a; auto; apply Min_leEq_lft.
Qed.

The following lemma is a bit more specific: it shows that we can also estimate the distance from the center of a compact interval to any of its points.

Lemma compact_bnd_AbsIR : ∀ x y d H,
compact (x [-]d) (x [+]d) H y → AbsIR (x [-]y) [<=] d.
Proof.
intros x y d H H0.
inversion_clear H0.
simpl in |- *; unfold ABSIR in |- ×.
apply Max_leEq.
apply shift_minus_leEq; apply shift_leEq_plus'; auto.
rstepl (y[-]x).
apply shift_minus_leEq.
astepr (x[+]d); auto.
Qed.

Finally, two more useful lemmas to prove inclusion of compact intervals. They will be necessary for the definition and proof of the elementary properties of the integral.

Lemma included2_compact : ∀ x y Hxy, Compact Hab x → Compact Hab y →
included (compact (Min x y) (Max x y) Hxy) (Compact Hab).
Proof.
do 3 intro. intros H H0.
inversion_clear H.
inversion_clear H0.
apply included_compact; split.
    apply leEq_Min; auto.
   apply leEq_transitive with y.
    apply Min_leEq_rht.
   auto.
  apply leEq_transitive with y.
   auto.
  apply rht_leEq_Max.
apply Max_leEq; auto.
Qed.

Lemma included3_compact : ∀ x y z Hxyz,
Compact Hab x → Compact Hab y → Compact Hab z →
included (compact (Min (Min x y) z) (Max (Max x y) z) Hxyz) (Compact Hab).
Proof.
do 4 intro. intros H H0 H1.
inversion_clear H.
inversion_clear H0.
inversion_clear H1.
apply included_compact; split.
    repeat apply leEq_Min; auto.
   apply leEq_transitive with z.
    apply Min_leEq_rht.
   auto.
  apply leEq_transitive with z.
   auto.
  apply rht_leEq_Max.
repeat apply Max_leEq; auto.
Qed.

End Compact.

Hint Resolve included_compact included2_compact included3_compact : included.