proposition: Lemma R_metric_is_metric: metric R_metric.
proof: Proof. constructor; intros; unfold R_metric in *. - replace (y-x) with (-(x-y)) by ring. apply Rabs_Ropp. - replace (z-x) with ((y-x) + (z-y)) by ring. apply Rabs_triang. - replace (x-x) with 0 by ring. exact Rabs_R0. - apply NNPP. intro. assert (y - x <> 0) by lra. now apply Rabs_no_R0 in H1. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals