-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.
-