X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fsandwich_corollary.ma;h=6b509a4a84ef7ba0e358739c21a1d5e9e008a20e;hb=5b83f526bc4c63424313df91173b844699eada96;hp=f41b65028b75574f89092d2f478c5a239004d354;hpb=954ed2eaf305a60d7e046206472bc0397a421ad2;p=helm.git

diff --git a/helm/software/matita/dama/sandwich_corollary.ma b/helm/software/matita/dama/sandwich_corollary.ma
index f41b65028..6b509a4a8 100644
--- a/helm/software/matita/dama/sandwich_corollary.ma
+++ b/helm/software/matita/dama/sandwich_corollary.ma
@@ -14,18 +14,12 @@
 
 include "sandwich.ma".
 
-include "metric_lattice.ma".
-
 (* 3.17 *)
 lemma tends_uniq:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.
-  ∀x,y:apart_of_metric_space ? ml. 
-  (* BUG: it inserts a compesoed coercion instead of an hand made one, 
-     what to do? prefer the human made one or allow to kill a coercion? 
-   *)
-     xn ⇝ x → xn ⇝ y → x ≈ y.
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x,y:ml. 
+     xn ⇝ x → xn ⇝ y → δ x y ≈ 0.
 intros (R ml xn x y H1 H2); unfold tends0 in H1 H2; unfold d2s in H1 H2;
-intro Axy; lapply (ap2delta R ml x y Axy) as ge0;
+intro Axy; lapply (ap_le_to_lt ??? (ap_symmetric ??? Axy) (mpositive ? ml ??)) as ge0;
 cases (H1 (δ x y/1) (divide_preserves_lt ??? ge0)) (n1 Hn1); clear H1; 
 cases (H2 (δ x y/1) (divide_preserves_lt ??? ge0)) (n2 Hn2); clear H2;
 letin N ≝ (S (n2 + n1));
@@ -42,4 +36,4 @@ change in H with ( δx y/1+ δx y/1< δx y/1+ δx y/1);
 apply (lt_coreflexive ?? H);
 qed.
 
-
+(* 3.18 *)