+axiom ltT : ∀R:real.∀a,b:R.Type.
+
+
+alias symbol "or" = "constructive or".
+definition rapart ≝ λR:real.λa,b:R.a < b ∨ b < a.
+
+notation "a # b" non associative with precedence 50 for
+ @{ 'apart $a $b}.
+notation "a \approx b" non associative with precedence 50 for
+ @{ 'napart $a $b}.
+interpretation "real apartness" 'apart a b =
+ (cic:/matita/lebesgue/rapart.con _ a b).
+interpretation "real non apartness" 'napart a b =
+ (cic:/matita/constructive_connectives/Not.con
+ (cic:/matita/lebesgue/rapart.con _ a b)).
+
+record is_semi_metric (R : real) (T : Type) (d : T → T → R): Prop ≝ {
+ sm_positive: ∀a,b:T. d a b ≤ 0;
+ sm_reflexive: ∀a. d a a ≈ 0;
+ sm_symmetric: ∀a,b. d a b ≈ d b a;
+ sm_tri_ineq: ∀a,b,c:T. d a b ≤ d a c + d c b
+}.
+
+record semimetric_set (R : real) : Type ≝ {