X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_space.ma;h=e2112d65b6511a7cb6d7c5af984455741c4c4f75;hb=3a5b9647787e1402f6886d41824f664db290963f;hp=d529af83cd16c05d7c96495b01c12363c7e8c745;hpb=a42d4bd78f10ac8fc725c50c193503a3f29b848f;p=helm.git

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index d529af83c..e2112d65b 100644
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -14,9 +14,9 @@
 
 set "baseuri" "cic:/matita/metric_space/".
 
-include "ordered_group.ma".
+include "ordered_divisible_group.ma".
 
-record metric_space (R : ogroup) : Type ≝ {
+record metric_space (R : todgroup) : Type ≝ {
   ms_carr :> Type;
   metric: ms_carr → ms_carr → R;
   mpositive: ∀a,b:ms_carr. 0 ≤ metric a b; 
@@ -34,7 +34,7 @@ interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _).
 definition apart_metric:=
   λR.λms:metric_space R.λa,b:ms.0 < δ a b.
 
-lemma apart_of_metric_space: ∀R:ogroup.metric_space R → apartness.
+lemma apart_of_metric_space: ∀R:todgroup.metric_space R → apartness.
 intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; unfold;
 [1: intros 2 (x H); cases H (H1 H2); 
     lapply (ap_rewr ???? (eq_sym ??? (mreflexive ??x)) H2);
@@ -48,3 +48,4 @@ 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.