From bb7af347df386afcd3ea2adea8e7e982e3a5a253 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Oct 2008 13:09:42 +0000
Subject: [PATCH] models ported

---
 .../matita/contribs/dama/dama/lebesgue.ma     | 63 +++++--------------
 .../models/nat_dedekind_sigma_complete.ma     | 41 ++++++------
 .../contribs/dama/dama/models/nat_lebesgue.ma |  8 +--
 .../dama/dama/models/nat_order_continuous.ma  | 12 ++--
 .../dama/dama/models/nat_ordered_uniform.ma   | 14 +++--
 .../dama/dama/property_exhaustivity.ma        | 10 ++-
 .../matita/contribs/dama/dama/supremum.ma     | 20 ++++--
 7 files changed, 75 insertions(+), 93 deletions(-)

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 1536476b0..251352d1f 100644
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -23,63 +23,28 @@ lemma order_converges_bigger_lowsegment:
   ∀C:ordered_set.
    ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s. 
      ∀x:C.∀p:order_converge C a x. 
-       ∀j. seg_l (os_l C) s (λl.le (os_l C) l (pi1exT23 ???? p j)).
+       ∀j. 𝕝_s ≤ (pi1exT23 ???? p j).
 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);rewrite <W;
-[ intro H2; cases (SSa (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);
-| intro H2; cases (SSa (seg_u_ 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 (SSa 𝕝_s H2) (w Hw); simplify in Hw;
+lapply (H (w+j)) as K; cases (cases_in_segment ? s ? K); apply H3; apply Hw;
 qed.   
   
+alias symbol "upp" = "uppper".
+alias symbol "leq" = "Ordered set less or equal than".
 lemma order_converges_smaller_upsegment:
   ∀C:ordered_set.
    ∀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).
+       ∀j. (pi2exT23 ???? p j) ≤ 𝕦_s.
 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);]
+intro H2; cases (SIa 𝕦_s H2) (w Hw); lapply (H (w+j)) as K; 
+cases (cases_in_segment ? s ? K); apply H1; apply Hw;  
 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.
-
 (* Theorem 3.10 *)
 theorem lebesgue_oc:
   ∀C:ordered_uniform_space.
@@ -95,12 +60,12 @@ generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
 cut (∀i.xi i ∈ s) as Hxi; [2:
   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
-  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (trans_under_upp ?? (xi i) (a i) K Pu);] clear H3;
+  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
+  simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
 cut (∀i.yi i ∈ s) as Hyi; [2:
   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (trans_under_low ?? (yi i) (a i) K Pl);] clear H2;
+  apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
 split;
 [1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
 |2: intros 3 (h);
@@ -136,12 +101,12 @@ generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
 cut (∀i.xi i ∈ s) as Hxi; [2:
   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
-  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (trans_under_upp ?? (xi i) (a i) K Pu);] clear H3;
+  lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
+  simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
 cut (∀i.yi i ∈ s) as Hyi; [2:
   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
-  apply (trans_under_low ?? (yi i) (a i) K Pl);] clear H2;
+  apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
 letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
 letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
 cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
index 9681b4d93..b65653dfe 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
@@ -18,8 +18,8 @@ include "nat/le_arith.ma".
 include "russell_support.ma".
 
 lemma hint1:
- ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u))
-   → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set l u))).
+ ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))
+   → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set s))).
 intros; assumption;
 qed.   
    
@@ -28,12 +28,13 @@ coercion hint1 nocomposites.
 alias symbol "pi1" = "exT \fst".
 alias symbol "N" = "ordered set N".
 lemma nat_dedekind_sigma_complete:
-  ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
+  ∀sg:‡ℕ.∀a:sequence {[sg]}.
+   a is_increasing → 
     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
-intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫; 
+intros 4; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫; 
 fold normalize X; intros; cases H1; 
 alias symbol "N" = "Natural numbers".
-letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j))); 
+letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ s = \fst (a j)) ∨ (i < 𝕦_sg ∧ s + i ≤ 𝕦_sg + \fst (a j))); 
 (* s - aj <= max 0 (u - i) *)  
 letin m ≝ (hide ? (
   let rec aux i ≝
@@ -49,17 +50,20 @@ letin m ≝ (hide ? (
    :
    ∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
 [3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
-    cases u in H2 Hs a ⊢ %; intros (a Hs H);
+    cases (cases_in_segment ??? Hs);
+    elim 𝕦_sg in H1 ⊢ %; intros (a Hs H);
     [1: left; split; [apply le_n]
         generalize in match H;
         generalize in match Hs;
         rewrite > (?:s = O); 
         [2: cases Hs; lapply (os_le_to_nat_le ?? H1);
             apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin).
-        |1: intros; lapply (os_le_to_nat_le (\fst (a O)) O (H2 O));
-            lapply (le_n_O_to_eq ? Hletin); assumption;]
+        |1: intros; unfold Type_of_ordered_set in sg;
+            lapply (H2 O) as K; lapply (sl2l ?? (a O) ≪s,Hs≫ K) as P;
+            simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
+            lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
     |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n];
-        apply (trans_le ??? (os_le_to_nat_le ?? H1));
+        apply (trans_le ??? (os_le_to_nat_le ?? H3));
         apply le_plus_n_r;] 
 |2: clear H6; cut (s = \fst (a (aux n1))); [2:
       cases (le_to_or_lt_eq ?? H5); [2: assumption]
@@ -72,9 +76,9 @@ letin m ≝ (hide ? (
     cases H5; clear H5; cases H7; clear H7;
     [1: left; split; [ apply (le_S ?? H5); | assumption]
     |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
-    |*: cases (cmp_nat u (S n1));
+    |*: cases (cmp_nat 𝕦_sg (S n1));
         [1,3: left; split; [1,3: assumption |2: assumption]
-            cut (u = S n1); [2: apply le_to_le_to_eq; assumption ]
+            cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ]
             clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
             cut (s = S (\fst (a w)));
             [2: apply le_to_le_to_eq; [2: assumption]
@@ -90,7 +94,7 @@ letin m ≝ (hide ? (
             [1: rewrite > sym_plus in ⊢ (? ? %);
                 rewrite < H6; apply le_plus_r; assumption;
             |2: cases (H3 (a w) H6);
-                change with (s + S n1 ≤ u + \fst (a w1));rewrite < plus_n_Sm;
+                change with (s + S n1 ≤ 𝕦_sg + \fst (a w1));rewrite < plus_n_Sm;
                 apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
                 apply (le_plus ???? (le_n ?) H9);]]]]
 clearbody m; unfold spec in m; clear spec;
@@ -103,14 +107,14 @@ letin find ≝ (
           | false ⇒ find (S i) w]]
  in find
  :
-  ∀i,bound.∃j.i + bound = u → s = \fst (a j));
+  ∀i,bound.∃j.i + bound = 𝕦_sg → s = \fst (a j));
 [1: cases (find (S n) n2); intro; change with (s = \fst (a w));
     apply H6; rewrite < H7; simplify; apply plus_n_Sm;
 |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
 |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
-    cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption]
+    cases (m 𝕦_sg); cases H4; clear H4; cases H5; clear H5; [assumption]
     cases (not_le_Sn_n ? H4)]
-clearbody find; cases (find O u);
+clearbody find; cases (find O 𝕦_sg);
 exists [apply w]; intros; change with (s = \fst (a j));
 rewrite > (H4 ?); [2: reflexivity]
 apply le_to_le_to_eq;
@@ -121,8 +125,8 @@ apply le_to_le_to_eq;
 qed.
 
 lemma hint2:
- ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u))
-   → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set l u))).
+ ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))
+   → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set s))).
 intros; assumption;
 qed.   
    
@@ -130,6 +134,5 @@ coercion hint2 nocomposites.
    
 alias symbol "N" = "ordered set N".
 axiom nat_dedekind_sigma_complete_r:
-  ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing → 
+  ∀s:‡ℕ.∀a:sequence {[s]}.a is_decreasing → 
     ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
-
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
index dd1f52b72..fd1d8dbcb 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
@@ -16,11 +16,11 @@ include "lebesgue.ma".
 include "models/nat_order_continuous.ma".
 
 theorem nat_lebesgue_oc:
-   ∀a:sequence ℕ.∀l,u:ℕ.∀H:∀i:nat.a i ∈ [l,u]. 
+   ∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s. 
      ∀x:ℕ.a order_converges x → 
-      x ∈ [l,u] ∧ 
-      ∀h:x ∈ [l,u].
-       uniform_converge {[l,u]} ⌊n,≪a n,H n≫⌋ ≪x,h≫.
+      x ∈ s ∧ 
+      ∀h:x ∈ s.
+       uniform_converge {[s]} ⌊n,≪a n,H n≫⌋ ≪x,h≫.
 intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption;
 qed.
 
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
index 7949ba2d2..0b4c92e3e 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
@@ -15,20 +15,20 @@
 include "models/nat_dedekind_sigma_complete.ma".
 include "models/nat_ordered_uniform.ma".
 
-lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity (segment_ordered_uniform_space ℕ l u).
-intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
-[1: cases (nat_dedekind_sigma_complete l u a H1 ? H2); 
+lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s).
+intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
+[1: cases (nat_dedekind_sigma_complete s a H1 ? H2); 
     exists [apply w1]; intros; 
-    apply (restrict nat_ordered_uniform_space l u ??? H4);     
+    apply (restrict nat_ordered_uniform_space s ??? H4);     
     generalize in match (H ? H5);
     cases x; intro; 
     generalize in match (refl_eq ? (a i):a i = a i);
     generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;  
     intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
     apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));
-|2: cases (nat_dedekind_sigma_complete_r l u a H1 ? H2); 
+|2: cases (nat_dedekind_sigma_complete_r s a H1 ? H2); 
     exists [apply w1]; intros; 
-    apply (restrict nat_ordered_uniform_space l u ??? H4);     
+    apply (restrict nat_ordered_uniform_space s ??? H4);     
     generalize in match (H ? H5);
     cases x; intro; 
     generalize in match (refl_eq ? (a i):a i = a i);
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma
index 82eedb35a..becbab2fb 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma
@@ -18,11 +18,15 @@ include "ordered_uniform.ma".
 
 definition nat_ordered_uniform_space:ordered_uniform_space.
  apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
-simplify; intros 7; cases H3; 
-cases H (_); cases (H8 y); apply H9; cases (H8 p);
-lapply (H12 H1) as H13; apply (le_le_eq);
-[1: apply (le_transitive ??? H4); apply (Le≪ ? H13); assumption;
-|2: apply (le_transitive ???? H5); apply (Le≫ ? (eq_sym ??? H13)); assumption;]
+simplify; intros 10;  cases H (_); cases (H7 y); apply H8; cases (H7 s);
+lapply (H11 H1) as H13; apply (le_le_eq);
+[2: apply (le_transitive ??? H5); apply (Le≪ ? H13); assumption;
+|1: assumption;
+|3: change with (le (os_r ℕ) (\snd y) (\fst y));
+    apply (ge_transitive ??? H5);apply (ge_transitive ???? H4);
+    change with (le (os_l ℕ) (\fst s) (\snd s));
+    apply (Le≫ ? H13); apply le_reflexive;
+|4: assumption;]
 qed. 
  
 interpretation "Ordered uniform space N" 'N = nat_ordered_uniform_space.
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 9788d4d35..7145b4288 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -68,8 +68,6 @@ definition exhaustive ≝
      (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.
@@ -80,13 +78,13 @@ lemma h_uparrow_to_in_segment:
 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}.
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).
-- 
2.39.2