+(* Definition 3.7 *)
+definition exhaustive ≝
+ λC:ordered_uniform_space.
+ ∀a,b:sequence C.
+ (a is_increasing → a is_upper_located → a is_cauchy) ∧
+ (b is_decreasing → b is_lower_located → b is_cauchy).
+
+lemma prove_in_segment:
+ ∀O:half_ordered_set.∀s:segment O.∀x:O.
+ seg_l O s (λl.l ≤≤ x) → seg_u O s (λu.x ≤≤ u) → x ∈ s.
+intros; unfold; cases (wloss_prop O); rewrite < H2;
+split; assumption;
+qed.
+
+lemma h_uparrow_to_in_segment:
+ ∀C:half_ordered_set.
+ ∀s:segment C.
+ ∀a:sequence C.
+ (∀i.a i ∈ s) →
+ ∀x:C. uparrow C a x →
+ in_segment C s x.
+intros (C H a H1 x H2); unfold in H2; cases H2; clear H2;unfold in H3 H4; cases H4; clear H4; unfold in H2;
+cases (wloss_prop C) (W W); apply prove_in_segment; unfold; rewrite <W;simplify;
+[ apply (hle_transitive ??? x ? (H2 O)); lapply (H1 O) as K; unfold in K; rewrite <W in K;
+ cases K; unfold in H4 H6; rewrite <W in H6 H4; simplify in H4 H6; assumption;
+| intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
+ cases K; unfold in H5 H4; rewrite<W in H4 H5; simplify in H4 H5; apply (H5 H6);
+| apply (hle_transitive ??? x ? (H2 O)); lapply (H1 0) as K; unfold in K; rewrite <W in K;
+ cases K; unfold in H4 H6; rewrite <W in H4 H6; simplify in H4 H6; assumption;
+| intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
+ cases K; unfold in H5 H4; rewrite<W in H4 H5; simplify in H4 H5; apply (H4 H6);]
+qed.
+
+notation "'uparrow_to_in_segment'" non associative with precedence 90 for @{'uparrow_to_in_segment}.
+notation "'downarrow_to_in_segment'" non associative with precedence 90 for @{'downarrow_to_in_segment}.
+
+interpretation "uparrow_to_in_segment" 'uparrow_to_in_segment = (h_uparrow_to_in_segment (os_l _)).
+interpretation "downarrow_to_in_segment" 'downarrow_to_in_segment = (h_uparrow_to_in_segment (os_r _)).
+