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;
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);