X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsupremum.ma;h=ca422597d5a9c7a98c8b5b18d9080294ab5c1eb9;hb=e2a6d130d5274760f4591197bbbc66c3191e8a6a;hp=e3a83a09a4f5d2d72646ee2a360b65ef82c03f90;hpb=5322d66340d43e85b85e15dddcddeff3ae3a3552;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index e3a83a09a..ca422597d 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -202,10 +202,10 @@ record segment (O : Type) : Type ≝ {
    seg_u_ : O
 }.
 
-notation > "𝕦_term 90 s" non associative with precedence 45 for @{'upp $s}.
-notation "𝕦 \sub term 90 s" non associative with precedence 45 for @{'upp $s}. 
-notation > "𝕝_term 90 s" non associative with precedence 45 for @{'low $s}.
-notation "𝕝 \sub term 90 s" non associative with precedence 45 for @{'low $s}. 
+notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}.
+notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}. 
+notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}.
+notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}. 
  
 definition seg_u ≝
  λO:half_ordered_set.λs:segment O.
@@ -340,6 +340,18 @@ whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?);
 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 qed.
 
+lemma l2sl:
+  ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
+intros; intro; apply H; apply sx2x; apply H1;
+qed.
+
+
+lemma sl2l:
+  ∀C,s.∀x,y:half_segment_ordered_set C s. x ≤≤ y → \fst x ≤≤ \fst y.
+intros; intro; apply H; apply x2sx; apply H1;
+qed.
+
+
 lemma h_segment_preserves_supremum:
   ∀O:half_ordered_set.∀s:segment O.
    ∀a:sequence (half_segment_ordered_set ? s).