yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!

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

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index 595407de868cd45a7b0b89b9e35f9c0e618ed2f8..bd16b2bd60217b33208159b97e188c99c2b06ee3 100644 (file)
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -47,7 +47,7 @@ intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric;
     apply (lt0plus_orlt ????? LT0); apply mpositive;]
 qed.
     
-coercion cic:/matita/metric_space/apart_of_metric_space.con.
+(* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
 
 lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.x#y → 0 < δ x y.
 intros 2 (R m); cases m 0; simplify; intros; assumption; qed.