proposition: Lemma id_is_isopsmetry : forall X : CPsMetricSpace, isopsmetry (id_un_op X).
proof: Proof. intro X. unfold isopsmetry in |- *. split. apply id_is_bij. unfold equivalent_psmetric in |- *. simpl in |- *. unfold id_un_op in |- *. split. split. apply CPsMetricSpace_is_CPsMetricSpace. apply Build_is_CPsMetricSpace. unfold com in |- *. intros x y. simpl in |- *. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. unfold nneg in |- *. simpl in |- *. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. unfold pos_imp_ap in |- *. simpl in |- *. apply ax_d_pos_imp_ap. apply CPsMetricSpace_is_CPsMetricSpace. unfold tri_ineq in |- *. simpl in |- *. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. split. exists 0. intros x y. simpl in |- *. astepr (OneR[*](x[-d]y)). astepr (x[-d]y). apply leEq_reflexive. exists 0. intros x y. simpl in |- *. astepr (OneR[*](x[-d]y)). astepr (x[-d]y). apply leEq_reflexive. Qed.
imports: CoRN.metrics.IR_CPMSpace