proposition: Lemma metric_ap_symmetric : forall X : CPsMetricSpace, Csymmetric (metric_ap X).
proof: Proof. intro X. unfold Csymmetric in |- *. intros x y. unfold metric_ap in |- *. intro H. astepr (x[-d]y). exact H. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv