fact: Record Metric_Space : Type := {Base : Type; dist : Base -> Base -> R; dist_pos : forall x y:Base, dist x y >= 0; dist_sym : forall x y:Base, dist x y = dist y x; dist_refl : forall x y:Base, dist x y = 0 <-> x = y; dist_tri : forall x y z:Base, dist x y <= dist x z + dist z y}.
imports: Rbase Rfunctions Lra