∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
∀x,h. uparrow C ⌊n,\fst (a n)⌋ x → uparrow (half_segment_ordered_set C s) a ≪x,h≫.
intros; cases H (Ha Hx); split;
-[ intro n; intro H; apply (Ha n); apply (sx2x ???? H);
+[ intro n; intro H; apply (Ha n); apply rule H;
| cases Hx; split;
- [ intro n; intro H; apply (H1 n);apply (sx2x ???? H);
- | intros; cases (H2 (\fst y)); [2: apply (sx2x ???? H3);]
- exists [apply w] apply (x2sx ?? (a w) y H4);]]
+ [ intro n; intro H; apply (H1 n);apply rule H;
+ | intros; cases (H2 (\fst y)); [2: apply rule H3;]
+ exists [apply w] apply (x2sx_ ?? (a w) y H4);]]
qed.
notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
(a is_increasing → a is_upper_located → a is_cauchy) ∧
(b is_decreasing → b is_lower_located → b is_cauchy).
-STOP
-
lemma h_uparrow_to_in_segment:
∀C:half_ordered_set.
∀s:segment C.
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;
[ 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;
+ cases K; unfold in H4 H6; apply H4;
| 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);
+ cases K; unfold in H5 H4; apply H5; apply 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;
+ cases K; unfold in H4 H6; apply H6;
| 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);]
+ cases K; unfold in H5 H4; apply (H4 H6);]
qed.
notation "'uparrow_to_in_segment'" non associative with precedence 90 for @{'uparrow_to_in_segment}.