proposition: Lemma MStotallybounded_totallybounded : forall (P : IR -> CProp) (H0 : {x : IR | P x}), pred_wd IR P -> MStotally_bounded (SubPsMetricSpace (X:=IR_as_CPsMetricSpace) P) -> totally_bounded P.
proof: Proof. intros P H0 Q. unfold MStotally_bounded in |- *. intro H. unfold totally_bounded in |- *. constructor. exact H0. intros e H1. set (H2 := OneR[/] e[//]ap_symmetric_unfolded IR [0] e (less_imp_ap IR [0] e H1)) in *. unfold AbsSmall in |- *. set (H3 := Archimedes H2) in *. elim H3. intros m H4. elim H with m. intros l H5. exists (list_IR P l). intro x. apply is_P. exact Q. intros x H6. generalize H5. simpl in |- *. intro H7. elim (H7 (from_IR P x H6)). intros x0 H8 H9. exists (to_IR P x0). apply member1. exact H8. split. generalize H9. unfold dIR_as_CSetoid_fun in |- *. unfold dIR in |- *. case x0. intros. simpl in |- *. apply leEq_transitive with ([--](one_div_succ (R:=IR) m)). apply inv_resp_leEq. unfold one_div_succ in |- *. apply shift_div_leEq. unfold Snring in |- *. apply less_transitive_unfolded with (nring (R:=IR) m). apply less_leEq_trans with H2. unfold H2 in |- *. apply recip_resp_pos. exact H1. exact H4. simpl in |- *. astepl (nring (R:=IR) m[+][0]). apply plus_resp_less_lft. apply pos_one. apply shift_leEq_mult' with (ap_symmetric_unfolded IR [0] e (less_imp_ap IR [0] e H1)). exact H1. apply leEq_transitive with (nring (R:=IR) m). exact H4. unfold Snring in |- *. simpl in |- *. apply less_leEq. astepl (nring (R:=IR) m[+][0]). apply plus_resp_less_lft. apply pos_one. apply inv_cancel_leEq. astepr (one_div_succ (R:=IR) m). apply leEq_transitive with (AbsIR (x[-]scs_elem)). apply inv_leEq_AbsIR. unfold AbsIR in |- *. simpl in |- *. generalize H10. simpl in |- *. intuition. generalize H9. case x0. intros x1 Q0 H10. simpl in |- *. apply leEq_transitive with (one_div_succ (R:=IR) m). generalize H10. unfold dIR_as_CSetoid_fun in |- *. unfold dIR in |- *. simpl in |- *. intro H11. apply leEq_transitive with (AbsIR (x[-]x1)). apply leEq_AbsIR. unfold AbsIR in |- *. simpl in |- *. exact H11. unfold one_div_succ in |- *. apply shift_div_leEq. unfold Snring in |- *. apply less_transitive_unfolded with (nring (R:=IR) m). apply less_leEq_trans with H2. unfold H2 in |- *. apply recip_resp_pos. exact H1. exact H4. simpl in |- *. astepl (nring (R:=IR) m[+][0]). apply plus_resp_less_lft. apply pos_one. apply shift_leEq_mult' with (ap_symmetric_unfolded IR [0] e (less_imp_ap IR [0] e H1)). exact H1. apply leEq_transitive with (nring (R:=IR) m). exact H4. unfold Snring in |- *. simpl in |- *. apply less_leEq. astepl (nring (R:=IR) m[+][0]). apply plus_resp_less_lft. apply pos_one. Qed.
imports: CoRN.metrics.Prod_Sub