X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fsandwich.ma;h=aaea369f55ce82c67dfbf186e67a31408d23fd58;hb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;hp=95dd0d3cbc0c5add6a783457b962f96e791509ce;hpb=6067115471521e8b9ea805531cb94a0a80774314;p=helm.git

diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma
index 95dd0d3cb..aaea369f5 100644
--- a/helm/software/matita/dama/sandwich.ma
+++ b/helm/software/matita/dama/sandwich.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/sandwich/".
+
 
 include "nat/plus.ma".
 include "nat/orders.ma".
@@ -26,21 +26,15 @@ lemma ltwr: ∀a,b,c:nat. a + b < c → a < c.
 intros 3 (x y z); rewrite > sym_plus; apply ltwl;
 qed. 
 
-include "sequence.ma".
+include "tend.ma".
 include "metric_lattice.ma".
 
-definition d2s ≝ 
-  λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
-
-notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
-  
-interpretation "tends to" 'tends s x = 
-  (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
-    
+alias symbol "leq" = "ordered sets less or equal than".
 alias symbol "and" = "constructive and".
 theorem sandwich:
+let ugo ≝ excess_OF_lattice1 in
   ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
-    (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) → 
+    (∀n. (xn n ≤ an n) ∧ (bn n ≤ xn n)) →  
     an ⇝ x → bn ⇝ x → xn ⇝ x.
 intros (R ml an bn xn x H Ha Hb); 
 unfold tends0 in Ha Hb ⊢ %; unfold d2s in Ha Hb ⊢ %; intros (e He);
@@ -54,16 +48,22 @@ cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2;
 (* the main inequality *)
 cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
   apply (le_transitive ???? (mtineq ???? (an n3)));
-  lapply (le_mtri ????? H7 H8) as H9; clear H7 H8;
-  lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
   cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2:
-    apply (Eq≈  (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
-    apply (Eq≈  (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
-    apply (Eq≈  (δ(an n3) (xn n3) +  (-δ(xn n3) (bn n3) +  δ(xn n3) (bn n3))) ? (opp_inverse ??));
-    apply (Eq≈  (δ(an n3) (xn n3) +  (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
-    apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear H10;
-  apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));    
-  apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
+    lapply (le_mtri ?? ??? H8 H7) as H9; clear H7 H8;
+    lapply (Eq≈ ? (msymmetric ????) H9) as H10; clear H9;
+    lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H10) as H9; clear H10;
+    apply (Eq≈ ? H9); clear H9;
+    apply (Eq≈ (δ(xn n3) (an n3)+ δ(bn n3) (xn n3)+- δ(xn n3) (bn n3)) (plus_comm ??( δ(xn n3) (an n3))));
+    apply (Eq≈ (δ(xn n3) (an n3)+ δ(bn n3) (xn n3)+- δ(bn n3) (xn n3)) (feq_opp ??? (msymmetric ????)));    
+    apply (Eq≈ ( δ(xn n3) (an n3)+ (δ(bn n3) (xn n3)+- δ(bn n3) (xn n3))) (plus_assoc ????));
+    apply (Eq≈ (δ(xn n3) (an n3) + (- δ(bn n3) (xn n3) + δ(bn n3) (xn n3))) (plus_comm ??(δ(bn n3) (xn n3))));
+    apply (Eq≈ (δ(xn n3) (an n3) + 0) (opp_inverse ??));
+    apply (Eq≈ ? (plus_comm ???));
+    apply (Eq≈ ? (zero_neutral ??));
+    apply (Eq≈ ? (msymmetric ????));
+    apply eq_reflexive;]
+  apply (Le≪ (δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));    
+  apply (Le≪ (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
   apply (Le≪ (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3))));
   apply (Le≪ (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
   apply (Le≪ ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));