proposition: Lemma compact_is_totally_bounded : forall a b Hab, totally_bounded (compact a b Hab).
proof: Proof. intros; split. exists a. apply compact_inc_lft. cut (forall (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 | forall x : IR, member x l -> compact a b Hab x | forall 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. exists l. assumption. intros x Hx; elim (Hl x Hx). intros y Hy Hy'. exists 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. exists (a::nil). intros x H1. inversion H1 as [H2 | H2]. elim H2. apply compact_wd with a; algebra. apply compact_inc_lft. intros. exists 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. exists (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. exists 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 *. exists (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. exists ((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. exists (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'. exists y. left; assumption. auto. try rename X into H2. inversion_clear H2; split. assumption. apply less_leEq; auto. exists 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.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists