...

[helm.git] / helm / software / matita / contribs / dama / dama / supremum.ma

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index ca422597d5a9c7a98c8b5b18d9080294ab5c1eb9..0de61b292fcaca3e40f5b7bddfa7ba0b88d27398 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -322,7 +322,7 @@ coercion hint_sequence3 nocomposites.
 
 (* Lemma 2.9 - non easily dualizable *)
 
-lemma x2sx:
+lemma x2sx_:
   ∀O:half_ordered_set.
    ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
     \fst x ≰≰ \fst y → x ≰≰ y.
@@ -331,7 +331,7 @@ whd in ⊢ (?→? (% ? ?)? ? ? ? ?); simplify in ⊢ (?→%);
 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 qed.
 
-lemma sx2x:
+lemma sx2x_:
   ∀O:half_ordered_set.
    ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
     x ≰≰ y → \fst x ≰≰ \fst y.
@@ -340,17 +340,21 @@ whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?);
 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 qed.
 
-lemma l2sl:
+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;
+intros; intro; apply H; apply sx2x_; apply H1;
 qed.
 
 
-lemma sl2l:
+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;
+intros; intro; apply H; apply x2sx_; apply H1;
 qed.
 
+coercion x2sx_ nocomposites.
+coercion sx2x_ nocomposites.
+coercion l2sl_ nocomposites.
+coercion sl2l_ nocomposites.
 
 lemma h_segment_preserves_supremum:
   ∀O:half_ordered_set.∀s:segment O.
@@ -360,13 +364,13 @@ lemma h_segment_preserves_supremum:
       supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x.
 intros; split; cases H; clear H; 
 [1: intro n; lapply (H1 n) as K; clear H1 H2;
-    intro; apply K; clear K; apply (sx2x ???? H);
+    intro; apply K; clear K; apply rule H; 
 |2: cases H2; split; clear H2;
     [1: intro n; lapply (H n) as K; intro W; apply K;
-        apply (sx2x ???? W);
+        apply rule W;
     |2: clear H1 H; intros (y0 Hy0); cases (H3 (\fst y0));[exists[apply w]]
-        [1: change in H with (\fst (a w) ≰≰ \fst y0); apply (x2sx ???? H);
-        |2: apply (sx2x ???? Hy0);]]]
+        [1: change in H with (\fst (a w) ≰≰ \fst y0); apply rule H;
+        |2: apply rule Hy0;]]]
 qed.
 
 notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.