Procedural : added some missing cases

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

diff --git a/helm/software/matita/dama/sandwich_corollary.ma b/helm/software/matita/dama/sandwich_corollary.ma
index 72da08236392c9d79b44be6462c732f55bc48641..6b509a4a84ef7ba0e358739c21a1d5e9e008a20e 100644 (file)
--- a/helm/software/matita/dama/sandwich_corollary.ma
+++ b/helm/software/matita/dama/sandwich_corollary.ma
@@ -14,15 +14,9 @@
 
 include "sandwich.ma".
 
-include "metric_lattice.ma".
-
 (* 3.17 *)
 lemma tends_uniq:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.
-  ∀x,y: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? 
-   *)
+  ∀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 (ap_le_to_lt ??? (ap_symmetric ??? Axy) (mpositive ? ml ??)) as ge0;