snopshot before isabellization

[helm.git] / helm / software / matita / dama / sandwich.ma

diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma
index 037d3d7dcb416c063b79d5136410ae0b3c900c33..47709bd24c78f5bbfd27b0d528decf4e6741dd4c 100644 (file)
--- a/helm/software/matita/dama/sandwich.ma
+++ b/helm/software/matita/dama/sandwich.ma
@@ -36,11 +36,12 @@ 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 "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. (le (excess_OF_lattice1 ml) (xn n) (an n)) ∧ 
+     (le (excess_OF_lattice1 ?) (bn n) (xn n))) → True. 
     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);
@@ -55,7 +56,7 @@ cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2;
 cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
   apply (le_transitive ???? (mtineq ???? (an n3)));
   cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2:
-    lapply (le_mtri ????? H7 H8) as H9; clear H7 H8;
+    lapply (le_mtri ?? ??? (ge_to_le ??? H7) (ge_to_le ??? H8)) as H9; clear H7 H8;
     lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
     apply (Eq≈ (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
     apply (Eq≈ (δ(an n3) (xn n3) + 0) ? (plus_comm ???));