- ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
- ∀x:C.∀p:a order_converges x.
- ∀j.(pi2exT23 ???? p) j ≤ u.
-intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
-cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
-intro H2; cases (H10 ? H2);
-cases (H (w1+j)); apply (H11 H7);
-qed.
-
+ ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
+ ∀x:C.∀p:order_converge C a x.
+ ∀j. seg_u (os_l C) s (λu.le (os_l C) (pi2exT23 ???? p j) u).
+intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
+cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
+cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
+cases (wloss_prop (os_l C))(W W); unfold os_r; unfold dual_hos; simplify;rewrite <W;
+[ intro H2; cases (SIa (seg_u_ (os_l C) s) H2) (w Hw); simplify in Hw;
+ lapply (H (w+j)) as K; unfold in K; whd in K:(? % ? ? ? ?); simplify in K:(%);
+ rewrite <W in K; cases K; whd in H3:(? % ? ? ? ?); simplify in H3:(%); rewrite <W in H3;
+ simplify in H3; apply (H3 Hw);
+| intro H2; cases (SIa (seg_l_ C s) H2) (w Hw); simplify in Hw;
+ lapply (H (w+j)) as K; unfold in K; whd in K:(? % ? ? ? ?); simplify in K:(%);
+ rewrite <W in K; cases K; whd in H1:(? % ? ? ? ?); simplify in H1:(%);
+ rewrite <W in H1; simplify in H1; apply (H1 Hw);]
+qed.
+
+alias symbol "upp" = "uppper".
+alias symbol "leq" = "Ordered set less or equal than".
+lemma cases_in_segment:
+ ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → seg_l C s (λl.l ≤≤ x) ∧ seg_u C s (λu.x ≤≤ u).
+intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
+cases H; split; assumption;
+qed.
+
+lemma trans_under_upp:
+ ∀O:ordered_set.∀s:‡O.∀x,y:O.
+ x ≤ y → 𝕦_s (λu.y ≤ u) → 𝕦_s (λu.x ≤ u).
+intros; cases (wloss_prop (os_l O)) (W W); unfold; unfold in H1; rewrite<W in H1 ⊢ %;
+apply (le_transitive ??? H H1);
+qed.
+
+lemma trans_under_low:
+ ∀O:ordered_set.∀s:‡O.∀x,y:O.
+ y ≤ x → 𝕝_s (λl.l ≤ y) → 𝕝_s (λl.l ≤ x).
+intros; cases (wloss_prop (os_l O)) (W W); unfold; unfold in H1; rewrite<W in H1 ⊢ %;
+apply (le_transitive ??? H1 H);
+qed.
+
+lemma l2sl:
+ ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
+intros; unfold in H ⊢ %; intro; apply H; clear H; unfold in H1 ⊢ %;
+cases (wloss_prop C) (W W); whd in H1:(? (% ? ?) ? ? ? ?); simplify in H1:(%);
+rewrite < W in H1 ⊢ %; apply H1;
+qed.
+